%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR036+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n027.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:07 PM UTC 2025 % Result : Theorem 20.84s 21.01s % Output : Proof 20.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.14 % Problem : CSR036+1 : TPTP v9.2.0. Released v3.4.0. % 0.09/0.15 % Command : duper %s % 0.15/0.37 % Computer : n027.cluster.edu % 0.15/0.37 % Model : x86_64 x86_64 % 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.37 % Memory : 8042.1875MB % 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.37 % CPULimit : 300 % 0.15/0.37 % WCLimit : 300 % 0.15/0.37 % DateTime : Thu Oct 2 19:44:39 EDT 2025 % 0.15/0.37 % CPUTime : % 20.84/21.01 SZS status Theorem for theBenchmark.p % 20.84/21.01 SZS output start Proof for theBenchmark.p % 20.84/21.01 Clause #5 (by assumption #[]): Eq (genls c_tptpcol_2_2 c_tptpcol_1_1) True % 20.84/21.01 Clause #7 (by assumption #[]): Eq (genls c_tptpcol_3_16386 c_tptpcol_2_2) True % 20.84/21.01 Clause #9 (by assumption #[]): Eq (genls c_tptpcol_4_16387 c_tptpcol_3_16386) True % 20.84/21.01 Clause #11 (by assumption #[]): Eq (genls c_tptpcol_5_20483 c_tptpcol_4_16387) True % 20.84/21.01 Clause #13 (by assumption #[]): Eq (genls c_tptpcol_6_20484 c_tptpcol_5_20483) True % 20.84/21.01 Clause #15 (by assumption #[]): Eq (genls c_tptpcol_7_21508 c_tptpcol_6_20484) True % 20.84/21.01 Clause #17 (by assumption #[]): Eq (genls c_tptpcol_8_22020 c_tptpcol_7_21508) True % 20.84/21.01 Clause #19 (by assumption #[]): Eq (genls c_tptpcol_9_22021 c_tptpcol_8_22020) True % 20.84/21.01 Clause #21 (by assumption #[]): Eq (genls c_tptpcol_10_22022 c_tptpcol_9_22021) True % 20.84/21.01 Clause #23 (by assumption #[]): Eq (genls c_tptpcol_11_22023 c_tptpcol_10_22022) True % 20.84/21.01 Clause #25 (by assumption #[]): Eq (genls c_tptpcol_12_22055 c_tptpcol_11_22023) True % 20.84/21.01 Clause #27 (by assumption #[]): Eq (genls c_tptpcol_13_22071 c_tptpcol_12_22055) True % 20.84/21.01 Clause #29 (by assumption #[]): Eq (genls c_tptpcol_14_22072 c_tptpcol_13_22071) True % 20.84/21.01 Clause #31 (by assumption #[]): Eq (genls c_tptpcol_15_22076 c_tptpcol_14_22072) True % 20.84/21.01 Clause #33 (by assumption #[]): Eq (genls c_tptpcol_2_65537 c_tptpcol_1_65536) True % 20.84/21.01 Clause #35 (by assumption #[]): Eq (genls c_tptpcol_3_65538 c_tptpcol_2_65537) True % 20.84/21.01 Clause #37 (by assumption #[]): Eq (genls c_tptpcol_4_65539 c_tptpcol_3_65538) True % 20.84/21.01 Clause #39 (by assumption #[]): Eq (genls c_tptpcol_5_69635 c_tptpcol_4_65539) True % 20.84/21.01 Clause #41 (by assumption #[]): Eq (genls c_tptpcol_6_71683 c_tptpcol_5_69635) True % 20.84/21.01 Clause #43 (by assumption #[]): Eq (genls c_tptpcol_7_72707 c_tptpcol_6_71683) True % 20.84/21.01 Clause #45 (by assumption #[]): Eq (genls c_tptpcol_8_72708 c_tptpcol_7_72707) True % 20.84/21.01 Clause #47 (by assumption #[]): Eq (genls c_tptpcol_9_72709 c_tptpcol_8_72708) True % 20.84/21.01 Clause #49 (by assumption #[]): Eq (genls c_tptpcol_10_72710 c_tptpcol_9_72709) True % 20.84/21.01 Clause #51 (by assumption #[]): Eq (genls c_tptpcol_11_72774 c_tptpcol_10_72710) True % 20.84/21.01 Clause #53 (by assumption #[]): Eq (genls c_tptpcol_12_72775 c_tptpcol_11_72774) True % 20.84/21.01 Clause #55 (by assumption #[]): Eq (genls c_tptpcol_13_72791 c_tptpcol_12_72775) True % 20.84/21.01 Clause #57 (by assumption #[]): Eq (genls c_tptpcol_14_72792 c_tptpcol_13_72791) True % 20.84/21.01 Clause #59 (by assumption #[]): Eq (genls c_tptpcol_15_72793 c_tptpcol_14_72792) True % 20.84/21.01 Clause #61 (by assumption #[]): Eq (genls c_tptpcol_16_72795 c_tptpcol_15_72793) True % 20.84/21.01 Clause #63 (by assumption #[]): Eq (disjointwith c_tptpcol_1_1 c_tptpcol_1_65536) True % 20.84/21.01 Clause #79 (by assumption #[]): Eq (∀ (X Y : Iota), disjointwith X Y → disjointwith Y X) True % 20.84/21.01 Clause #80 (by assumption #[]): Eq (∀ (ARG1 OLD NEW : Iota), And (disjointwith ARG1 OLD) (genls NEW OLD) → disjointwith ARG1 NEW) True % 20.84/21.01 Clause #81 (by assumption #[]): Eq (∀ (OLD ARG2 NEW : Iota), And (disjointwith OLD ARG2) (genls NEW OLD) → disjointwith NEW ARG2) True % 20.84/21.01 Clause #146 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (genls X Y) (genls Y Z) → genls X Z) True % 20.84/21.01 Clause #161 (by assumption #[]): Eq (Not (mtvisible c_tptp_member974_mt → disjointwith c_tptpcol_15_22076 c_tptpcol_16_72795)) True % 20.84/21.01 Clause #463 (by clausification #[79]): ∀ (a : Iota), Eq (∀ (Y : Iota), disjointwith a Y → disjointwith Y a) True % 20.84/21.01 Clause #464 (by clausification #[463]): ∀ (a a_1 : Iota), Eq (disjointwith a a_1 → disjointwith a_1 a) True % 20.84/21.01 Clause #465 (by clausification #[464]): ∀ (a a_1 : Iota), Or (Eq (disjointwith a a_1) False) (Eq (disjointwith a_1 a) True) % 20.84/21.01 Clause #466 (by superposition #[465, 63]): Or (Eq (disjointwith c_tptpcol_1_65536 c_tptpcol_1_1) True) (Eq False True) % 20.84/21.01 Clause #477 (by clausification #[80]): ∀ (a : Iota), Eq (∀ (OLD NEW : Iota), And (disjointwith a OLD) (genls NEW OLD) → disjointwith a NEW) True % 20.84/21.01 Clause #478 (by clausification #[477]): ∀ (a a_1 : Iota), Eq (∀ (NEW : Iota), And (disjointwith a a_1) (genls NEW a_1) → disjointwith a NEW) True % 20.84/21.01 Clause #479 (by clausification #[478]): ∀ (a a_1 a_2 : Iota), Eq (And (disjointwith a a_1) (genls a_2 a_1) → disjointwith a a_2) True % 20.87/21.04 Clause #480 (by clausification #[479]): ∀ (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) % 20.87/21.04 Clause #481 (by clausification #[480]): ∀ (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)) % 20.87/21.04 Clause #493 (by clausification #[81]): ∀ (a : Iota), Eq (∀ (ARG2 NEW : Iota), And (disjointwith a ARG2) (genls NEW a) → disjointwith NEW ARG2) True % 20.87/21.04 Clause #494 (by clausification #[493]): ∀ (a a_1 : Iota), Eq (∀ (NEW : Iota), And (disjointwith a a_1) (genls NEW a) → disjointwith NEW a_1) True % 20.87/21.04 Clause #495 (by clausification #[494]): ∀ (a a_1 a_2 : Iota), Eq (And (disjointwith a a_1) (genls a_2 a) → disjointwith a_2 a_1) True % 20.87/21.04 Clause #496 (by clausification #[495]): ∀ (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) % 20.87/21.04 Clause #497 (by clausification #[496]): ∀ (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)) % 20.87/21.04 Clause #598 (by clausification #[466]): Eq (disjointwith c_tptpcol_1_65536 c_tptpcol_1_1) True % 20.87/21.04 Clause #602 (by superposition #[598, 481]): ∀ (a : Iota), Or (Eq (disjointwith c_tptpcol_1_65536 a) True) (Or (Eq True False) (Eq (genls a c_tptpcol_1_1) False)) % 20.87/21.04 Clause #635 (by clausification #[161]): Eq (mtvisible c_tptp_member974_mt → disjointwith c_tptpcol_15_22076 c_tptpcol_16_72795) False % 20.87/21.04 Clause #637 (by clausification #[635]): Eq (disjointwith c_tptpcol_15_22076 c_tptpcol_16_72795) False % 20.87/21.04 Clause #642 (by clausification #[146]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (genls a Y) (genls Y Z) → genls a Z) True % 20.87/21.04 Clause #643 (by clausification #[642]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (genls a a_1) (genls a_1 Z) → genls a Z) True % 20.87/21.04 Clause #644 (by clausification #[643]): ∀ (a a_1 a_2 : Iota), Eq (And (genls a a_1) (genls a_1 a_2) → genls a a_2) True % 20.87/21.04 Clause #645 (by clausification #[644]): ∀ (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) % 20.87/21.04 Clause #646 (by clausification #[645]): ∀ (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)) % 20.87/21.04 Clause #647 (by superposition #[646, 7]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_3_16386 a) True) (Or (Eq (genls c_tptpcol_2_2 a) False) (Eq False True)) % 20.87/21.04 Clause #649 (by superposition #[646, 15]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_21508 a) True) (Or (Eq (genls c_tptpcol_6_20484 a) False) (Eq False True)) % 20.87/21.04 Clause #650 (by superposition #[646, 11]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_20483 a) True) (Or (Eq (genls c_tptpcol_4_16387 a) False) (Eq False True)) % 20.87/21.04 Clause #652 (by superposition #[646, 13]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_20484 a) True) (Or (Eq (genls c_tptpcol_5_20483 a) False) (Eq False True)) % 20.87/21.04 Clause #653 (by superposition #[646, 31]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_15_22076 a) True) (Or (Eq (genls c_tptpcol_14_22072 a) False) (Eq False True)) % 20.87/21.04 Clause #654 (by superposition #[646, 29]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_22072 a) True) (Or (Eq (genls c_tptpcol_13_22071 a) False) (Eq False True)) % 20.87/21.04 Clause #655 (by superposition #[646, 23]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_22023 a) True) (Or (Eq (genls c_tptpcol_10_22022 a) False) (Eq False True)) % 20.87/21.04 Clause #656 (by superposition #[646, 27]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_22071 a) True) (Or (Eq (genls c_tptpcol_12_22055 a) False) (Eq False True)) % 20.87/21.04 Clause #657 (by superposition #[646, 19]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_22021 a) True) (Or (Eq (genls c_tptpcol_8_22020 a) False) (Eq False True)) % 20.87/21.04 Clause #658 (by superposition #[646, 25]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_12_22055 a) True) (Or (Eq (genls c_tptpcol_11_22023 a) False) (Eq False True)) % 20.87/21.04 Clause #659 (by superposition #[646, 21]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_10_22022 a) True) (Or (Eq (genls c_tptpcol_9_22021 a) False) (Eq False True)) % 20.87/21.04 Clause #660 (by superposition #[646, 17]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_22020 a) True) (Or (Eq (genls c_tptpcol_7_21508 a) False) (Eq False True)) % 20.87/21.06 Clause #661 (by superposition #[646, 59]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_15_72793 a) True) (Or (Eq (genls c_tptpcol_14_72792 a) False) (Eq False True)) % 20.87/21.06 Clause #662 (by superposition #[646, 61]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_16_72795 a) True) (Or (Eq (genls c_tptpcol_15_72793 a) False) (Eq False True)) % 20.87/21.06 Clause #663 (by superposition #[646, 57]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_72792 a) True) (Or (Eq (genls c_tptpcol_13_72791 a) False) (Eq False True)) % 20.87/21.06 Clause #664 (by superposition #[646, 47]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_72709 a) True) (Or (Eq (genls c_tptpcol_8_72708 a) False) (Eq False True)) % 20.87/21.06 Clause #665 (by superposition #[646, 45]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_72708 a) True) (Or (Eq (genls c_tptpcol_7_72707 a) False) (Eq False True)) % 20.87/21.06 Clause #666 (by superposition #[646, 55]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_72791 a) True) (Or (Eq (genls c_tptpcol_12_72775 a) False) (Eq False True)) % 20.87/21.06 Clause #667 (by superposition #[646, 53]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_12_72775 a) True) (Or (Eq (genls c_tptpcol_11_72774 a) False) (Eq False True)) % 20.87/21.06 Clause #668 (by superposition #[646, 39]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_69635 a) True) (Or (Eq (genls c_tptpcol_4_65539 a) False) (Eq False True)) % 20.87/21.06 Clause #669 (by superposition #[646, 51]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_72774 a) True) (Or (Eq (genls c_tptpcol_10_72710 a) False) (Eq False True)) % 20.87/21.06 Clause #670 (by superposition #[646, 43]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_72707 a) True) (Or (Eq (genls c_tptpcol_6_71683 a) False) (Eq False True)) % 20.87/21.06 Clause #671 (by superposition #[646, 49]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_10_72710 a) True) (Or (Eq (genls c_tptpcol_9_72709 a) False) (Eq False True)) % 20.87/21.06 Clause #672 (by superposition #[646, 35]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_3_65538 a) True) (Or (Eq (genls c_tptpcol_2_65537 a) False) (Eq False True)) % 20.87/21.06 Clause #674 (by superposition #[646, 37]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_4_65539 a) True) (Or (Eq (genls c_tptpcol_3_65538 a) False) (Eq False True)) % 20.87/21.06 Clause #675 (by superposition #[646, 41]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_71683 a) True) (Or (Eq (genls c_tptpcol_5_69635 a) False) (Eq False True)) % 20.87/21.06 Clause #796 (by clausification #[602]): ∀ (a : Iota), Or (Eq (disjointwith c_tptpcol_1_65536 a) True) (Eq (genls a c_tptpcol_1_1) False) % 20.87/21.06 Clause #816 (by clausification #[647]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_3_16386 a) True) (Eq (genls c_tptpcol_2_2 a) False) % 20.87/21.06 Clause #817 (by superposition #[816, 5]): Or (Eq (genls c_tptpcol_3_16386 c_tptpcol_1_1) True) (Eq False True) % 20.87/21.06 Clause #819 (by clausification #[817]): Eq (genls c_tptpcol_3_16386 c_tptpcol_1_1) True % 20.87/21.06 Clause #821 (by superposition #[819, 796]): Or (Eq (disjointwith c_tptpcol_1_65536 c_tptpcol_3_16386) True) (Eq True False) % 20.87/21.06 Clause #836 (by clausification #[821]): Eq (disjointwith c_tptpcol_1_65536 c_tptpcol_3_16386) True % 20.87/21.06 Clause #839 (by superposition #[836, 481]): ∀ (a : Iota), % 20.87/21.06 Or (Eq (disjointwith c_tptpcol_1_65536 a) True) (Or (Eq True False) (Eq (genls a c_tptpcol_3_16386) False)) % 20.87/21.06 Clause #846 (by clausification #[649]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_21508 a) True) (Eq (genls c_tptpcol_6_20484 a) False) % 20.87/21.06 Clause #851 (by clausification #[839]): ∀ (a : Iota), Or (Eq (disjointwith c_tptpcol_1_65536 a) True) (Eq (genls a c_tptpcol_3_16386) False) % 20.87/21.06 Clause #859 (by clausification #[650]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_20483 a) True) (Eq (genls c_tptpcol_4_16387 a) False) % 20.87/21.06 Clause #860 (by superposition #[859, 9]): Or (Eq (genls c_tptpcol_5_20483 c_tptpcol_3_16386) True) (Eq False True) % 20.87/21.06 Clause #862 (by clausification #[860]): Eq (genls c_tptpcol_5_20483 c_tptpcol_3_16386) True % 20.87/21.06 Clause #899 (by clausification #[652]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_20484 a) True) (Eq (genls c_tptpcol_5_20483 a) False) % 20.87/21.06 Clause #902 (by superposition #[899, 862]): Or (Eq (genls c_tptpcol_6_20484 c_tptpcol_3_16386) True) (Eq False True) % 20.87/21.08 Clause #925 (by clausification #[653]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_15_22076 a) True) (Eq (genls c_tptpcol_14_22072 a) False) % 20.87/21.08 Clause #935 (by clausification #[654]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_22072 a) True) (Eq (genls c_tptpcol_13_22071 a) False) % 20.87/21.08 Clause #953 (by clausification #[655]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_22023 a) True) (Eq (genls c_tptpcol_10_22022 a) False) % 20.87/21.08 Clause #968 (by clausification #[656]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_22071 a) True) (Eq (genls c_tptpcol_12_22055 a) False) % 20.87/21.08 Clause #979 (by clausification #[657]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_22021 a) True) (Eq (genls c_tptpcol_8_22020 a) False) % 20.87/21.08 Clause #984 (by clausification #[902]): Eq (genls c_tptpcol_6_20484 c_tptpcol_3_16386) True % 20.87/21.08 Clause #985 (by superposition #[984, 846]): Or (Eq (genls c_tptpcol_7_21508 c_tptpcol_3_16386) True) (Eq True False) % 20.87/21.08 Clause #987 (by clausification #[985]): Eq (genls c_tptpcol_7_21508 c_tptpcol_3_16386) True % 20.87/21.08 Clause #989 (by clausification #[658]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_12_22055 a) True) (Eq (genls c_tptpcol_11_22023 a) False) % 20.87/21.08 Clause #1004 (by clausification #[659]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_10_22022 a) True) (Eq (genls c_tptpcol_9_22021 a) False) % 20.87/21.08 Clause #1023 (by clausification #[660]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_22020 a) True) (Eq (genls c_tptpcol_7_21508 a) False) % 20.87/21.08 Clause #1029 (by superposition #[1023, 987]): Or (Eq (genls c_tptpcol_8_22020 c_tptpcol_3_16386) True) (Eq False True) % 20.87/21.08 Clause #1030 (by clausification #[1029]): Eq (genls c_tptpcol_8_22020 c_tptpcol_3_16386) True % 20.87/21.08 Clause #1032 (by superposition #[1030, 979]): Or (Eq (genls c_tptpcol_9_22021 c_tptpcol_3_16386) True) (Eq True False) % 20.87/21.08 Clause #1034 (by clausification #[1032]): Eq (genls c_tptpcol_9_22021 c_tptpcol_3_16386) True % 20.87/21.08 Clause #1036 (by superposition #[1034, 1004]): Or (Eq (genls c_tptpcol_10_22022 c_tptpcol_3_16386) True) (Eq True False) % 20.87/21.08 Clause #1038 (by clausification #[1036]): Eq (genls c_tptpcol_10_22022 c_tptpcol_3_16386) True % 20.87/21.08 Clause #1040 (by superposition #[1038, 953]): Or (Eq (genls c_tptpcol_11_22023 c_tptpcol_3_16386) True) (Eq True False) % 20.87/21.08 Clause #1042 (by clausification #[1040]): Eq (genls c_tptpcol_11_22023 c_tptpcol_3_16386) True % 20.87/21.08 Clause #1044 (by superposition #[1042, 989]): Or (Eq (genls c_tptpcol_12_22055 c_tptpcol_3_16386) True) (Eq True False) % 20.87/21.08 Clause #1046 (by clausification #[1044]): Eq (genls c_tptpcol_12_22055 c_tptpcol_3_16386) True % 20.87/21.08 Clause #1048 (by superposition #[1046, 968]): Or (Eq (genls c_tptpcol_13_22071 c_tptpcol_3_16386) True) (Eq True False) % 20.87/21.08 Clause #1050 (by clausification #[661]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_15_72793 a) True) (Eq (genls c_tptpcol_14_72792 a) False) % 20.87/21.08 Clause #1055 (by clausification #[1048]): Eq (genls c_tptpcol_13_22071 c_tptpcol_3_16386) True % 20.87/21.08 Clause #1057 (by superposition #[1055, 935]): Or (Eq (genls c_tptpcol_14_22072 c_tptpcol_3_16386) True) (Eq True False) % 20.87/21.08 Clause #1059 (by clausification #[1057]): Eq (genls c_tptpcol_14_22072 c_tptpcol_3_16386) True % 20.87/21.08 Clause #1061 (by superposition #[1059, 925]): Or (Eq (genls c_tptpcol_15_22076 c_tptpcol_3_16386) True) (Eq True False) % 20.87/21.08 Clause #1063 (by clausification #[1061]): Eq (genls c_tptpcol_15_22076 c_tptpcol_3_16386) True % 20.87/21.08 Clause #1064 (by superposition #[1063, 851]): Or (Eq (disjointwith c_tptpcol_1_65536 c_tptpcol_15_22076) True) (Eq True False) % 20.87/21.08 Clause #1066 (by clausification #[662]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_16_72795 a) True) (Eq (genls c_tptpcol_15_72793 a) False) % 20.87/21.08 Clause #1072 (by clausification #[1064]): Eq (disjointwith c_tptpcol_1_65536 c_tptpcol_15_22076) True % 20.87/21.08 Clause #1076 (by superposition #[1072, 497]): ∀ (a : Iota), % 20.87/21.08 Or (Eq (disjointwith a c_tptpcol_15_22076) True) (Or (Eq True False) (Eq (genls a c_tptpcol_1_65536) False)) % 20.87/21.08 Clause #1087 (by clausification #[663]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_72792 a) True) (Eq (genls c_tptpcol_13_72791 a) False) % 20.87/21.08 Clause #1103 (by clausification #[664]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_72709 a) True) (Eq (genls c_tptpcol_8_72708 a) False) % 20.87/21.08 Clause #1110 (by clausification #[665]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_72708 a) True) (Eq (genls c_tptpcol_7_72707 a) False) % 20.87/21.10 Clause #1128 (by clausification #[666]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_72791 a) True) (Eq (genls c_tptpcol_12_72775 a) False) % 20.87/21.10 Clause #1142 (by clausification #[667]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_12_72775 a) True) (Eq (genls c_tptpcol_11_72774 a) False) % 20.87/21.10 Clause #1157 (by clausification #[668]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_69635 a) True) (Eq (genls c_tptpcol_4_65539 a) False) % 20.87/21.10 Clause #1164 (by clausification #[669]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_72774 a) True) (Eq (genls c_tptpcol_10_72710 a) False) % 20.87/21.10 Clause #1179 (by clausification #[670]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_72707 a) True) (Eq (genls c_tptpcol_6_71683 a) False) % 20.87/21.10 Clause #1193 (by clausification #[671]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_10_72710 a) True) (Eq (genls c_tptpcol_9_72709 a) False) % 20.87/21.10 Clause #1214 (by clausification #[672]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_3_65538 a) True) (Eq (genls c_tptpcol_2_65537 a) False) % 20.87/21.10 Clause #1215 (by superposition #[1214, 33]): Or (Eq (genls c_tptpcol_3_65538 c_tptpcol_1_65536) True) (Eq False True) % 20.87/21.10 Clause #1217 (by clausification #[1215]): Eq (genls c_tptpcol_3_65538 c_tptpcol_1_65536) True % 20.87/21.10 Clause #1240 (by clausification #[674]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_4_65539 a) True) (Eq (genls c_tptpcol_3_65538 a) False) % 20.87/21.10 Clause #1243 (by superposition #[1240, 1217]): Or (Eq (genls c_tptpcol_4_65539 c_tptpcol_1_65536) True) (Eq False True) % 20.87/21.10 Clause #1244 (by clausification #[1243]): Eq (genls c_tptpcol_4_65539 c_tptpcol_1_65536) True % 20.87/21.10 Clause #1247 (by superposition #[1244, 1157]): Or (Eq (genls c_tptpcol_5_69635 c_tptpcol_1_65536) True) (Eq True False) % 20.87/21.10 Clause #1249 (by clausification #[1247]): Eq (genls c_tptpcol_5_69635 c_tptpcol_1_65536) True % 20.87/21.10 Clause #1263 (by clausification #[675]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_71683 a) True) (Eq (genls c_tptpcol_5_69635 a) False) % 20.87/21.10 Clause #1267 (by superposition #[1263, 1249]): Or (Eq (genls c_tptpcol_6_71683 c_tptpcol_1_65536) True) (Eq False True) % 20.87/21.10 Clause #1268 (by clausification #[1267]): Eq (genls c_tptpcol_6_71683 c_tptpcol_1_65536) True % 20.87/21.10 Clause #1271 (by superposition #[1268, 1179]): Or (Eq (genls c_tptpcol_7_72707 c_tptpcol_1_65536) True) (Eq True False) % 20.87/21.10 Clause #1273 (by clausification #[1271]): Eq (genls c_tptpcol_7_72707 c_tptpcol_1_65536) True % 20.87/21.10 Clause #1276 (by superposition #[1273, 1110]): Or (Eq (genls c_tptpcol_8_72708 c_tptpcol_1_65536) True) (Eq True False) % 20.87/21.10 Clause #1278 (by clausification #[1276]): Eq (genls c_tptpcol_8_72708 c_tptpcol_1_65536) True % 20.87/21.10 Clause #1281 (by superposition #[1278, 1103]): Or (Eq (genls c_tptpcol_9_72709 c_tptpcol_1_65536) True) (Eq True False) % 20.87/21.10 Clause #1283 (by clausification #[1281]): Eq (genls c_tptpcol_9_72709 c_tptpcol_1_65536) True % 20.87/21.10 Clause #1286 (by superposition #[1283, 1193]): Or (Eq (genls c_tptpcol_10_72710 c_tptpcol_1_65536) True) (Eq True False) % 20.87/21.10 Clause #1288 (by clausification #[1286]): Eq (genls c_tptpcol_10_72710 c_tptpcol_1_65536) True % 20.87/21.10 Clause #1291 (by superposition #[1288, 1164]): Or (Eq (genls c_tptpcol_11_72774 c_tptpcol_1_65536) True) (Eq True False) % 20.87/21.10 Clause #1294 (by clausification #[1291]): Eq (genls c_tptpcol_11_72774 c_tptpcol_1_65536) True % 20.87/21.10 Clause #1297 (by superposition #[1294, 1142]): Or (Eq (genls c_tptpcol_12_72775 c_tptpcol_1_65536) True) (Eq True False) % 20.87/21.10 Clause #1299 (by clausification #[1297]): Eq (genls c_tptpcol_12_72775 c_tptpcol_1_65536) True % 20.87/21.10 Clause #1302 (by superposition #[1299, 1128]): Or (Eq (genls c_tptpcol_13_72791 c_tptpcol_1_65536) True) (Eq True False) % 20.87/21.10 Clause #1304 (by clausification #[1302]): Eq (genls c_tptpcol_13_72791 c_tptpcol_1_65536) True % 20.87/21.10 Clause #1307 (by superposition #[1304, 1087]): Or (Eq (genls c_tptpcol_14_72792 c_tptpcol_1_65536) True) (Eq True False) % 20.87/21.10 Clause #1309 (by clausification #[1307]): Eq (genls c_tptpcol_14_72792 c_tptpcol_1_65536) True % 20.87/21.10 Clause #1312 (by superposition #[1309, 1050]): Or (Eq (genls c_tptpcol_15_72793 c_tptpcol_1_65536) True) (Eq True False) % 20.87/21.10 Clause #1314 (by clausification #[1312]): Eq (genls c_tptpcol_15_72793 c_tptpcol_1_65536) True % 20.87/21.12 Clause #1317 (by superposition #[1314, 1066]): Or (Eq (genls c_tptpcol_16_72795 c_tptpcol_1_65536) True) (Eq True False) % 20.87/21.12 Clause #1320 (by clausification #[1317]): Eq (genls c_tptpcol_16_72795 c_tptpcol_1_65536) True % 20.87/21.12 Clause #3298 (by clausification #[1076]): ∀ (a : Iota), Or (Eq (disjointwith a c_tptpcol_15_22076) True) (Eq (genls a c_tptpcol_1_65536) False) % 20.87/21.12 Clause #3312 (by superposition #[3298, 1320]): Or (Eq (disjointwith c_tptpcol_16_72795 c_tptpcol_15_22076) True) (Eq False True) % 20.87/21.12 Clause #3313 (by clausification #[3312]): Eq (disjointwith c_tptpcol_16_72795 c_tptpcol_15_22076) True % 20.87/21.12 Clause #3315 (by superposition #[3313, 465]): Or (Eq True False) (Eq (disjointwith c_tptpcol_15_22076 c_tptpcol_16_72795) True) % 20.87/21.12 Clause #3318 (by clausification #[3315]): Eq (disjointwith c_tptpcol_15_22076 c_tptpcol_16_72795) True % 20.87/21.12 Clause #3319 (by superposition #[3318, 637]): Eq True False % 20.87/21.12 Clause #3324 (by clausification #[3319]): False % 20.87/21.12 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------