%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : REL023+1 : TPTP v9.2.0. Released v4.0.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:58:36 PM UTC 2025 % Result : Theorem 45.57s 45.73s % Output : Proof 45.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : REL023+1 : TPTP v9.2.0. Released v4.0.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n006.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 11:58:53 EDT 2025 % 0.13/0.34 % CPUTime : % 45.57/45.73 SZS status Theorem for theBenchmark.p % 45.57/45.73 SZS output start Proof for theBenchmark.p % 45.57/45.73 Clause #0 (by assumption #[]): Eq (∀ (X0 X1 : Iota), Eq (join X0 X1) (join X1 X0)) True % 45.57/45.73 Clause #1 (by assumption #[]): Eq (∀ (X0 X1 X2 : Iota), Eq (join X0 (join X1 X2)) (join (join X0 X1) X2)) True % 45.57/45.73 Clause #2 (by assumption #[]): Eq % 45.57/45.73 (∀ (X0 X1 : Iota), % 45.57/45.73 Eq X0 (join (complement (join (complement X0) (complement X1))) (complement (join (complement X0) X1)))) % 45.57/45.73 True % 45.57/45.73 Clause #3 (by assumption #[]): Eq (∀ (X0 X1 : Iota), Eq (meet X0 X1) (complement (join (complement X0) (complement X1)))) True % 45.57/45.73 Clause #5 (by assumption #[]): Eq (∀ (X0 : Iota), Eq (composition X0 one) X0) True % 45.57/45.73 Clause #6 (by assumption #[]): Eq (∀ (X0 X1 X2 : Iota), Eq (composition (join X0 X1) X2) (join (composition X0 X2) (composition X1 X2))) True % 45.57/45.73 Clause #7 (by assumption #[]): Eq (∀ (X0 : Iota), Eq (converse (converse X0)) X0) True % 45.57/45.73 Clause #9 (by assumption #[]): Eq (∀ (X0 X1 : Iota), Eq (converse (composition X0 X1)) (composition (converse X1) (converse X0))) True % 45.57/45.73 Clause #10 (by assumption #[]): Eq % 45.57/45.73 (∀ (X0 X1 : Iota), % 45.57/45.73 Eq (join (composition (converse X0) (complement (composition X0 X1))) (complement X1)) (complement X1)) % 45.57/45.73 True % 45.57/45.73 Clause #11 (by assumption #[]): Eq (∀ (X0 : Iota), Eq top (join X0 (complement X0))) True % 45.57/45.73 Clause #12 (by assumption #[]): Eq (∀ (X0 : Iota), Eq zero (meet X0 (complement X0))) True % 45.57/45.73 Clause #13 (by assumption #[]): Eq % 45.57/45.73 (Not % 45.57/45.73 (∀ (X0 X1 X2 : Iota), % 45.57/45.73 Eq (join (composition (meet X0 (converse X1)) (meet X1 X2)) (composition X0 (meet X1 X2))) % 45.57/45.73 (composition X0 (meet X1 X2)))) % 45.57/45.73 True % 45.57/45.73 Clause #14 (by clausification #[7]): ∀ (a : Iota), Eq (Eq (converse (converse a)) a) True % 45.57/45.73 Clause #15 (by clausification #[14]): ∀ (a : Iota), Eq (converse (converse a)) a % 45.57/45.73 Clause #16 (by clausification #[5]): ∀ (a : Iota), Eq (Eq (composition a one) a) True % 45.57/45.73 Clause #17 (by clausification #[16]): ∀ (a : Iota), Eq (composition a one) a % 45.57/45.73 Clause #18 (by clausification #[12]): ∀ (a : Iota), Eq (Eq zero (meet a (complement a))) True % 45.57/45.73 Clause #19 (by clausification #[18]): ∀ (a : Iota), Eq zero (meet a (complement a)) % 45.57/45.73 Clause #20 (by clausification #[11]): ∀ (a : Iota), Eq (Eq top (join a (complement a))) True % 45.57/45.73 Clause #21 (by clausification #[20]): ∀ (a : Iota), Eq top (join a (complement a)) % 45.57/45.73 Clause #22 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (X1 : Iota), Eq (join a X1) (join X1 a)) True % 45.57/45.73 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), Eq (Eq (join a a_1) (join a_1 a)) True % 45.57/45.73 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), Eq (join a a_1) (join a_1 a) % 45.57/45.73 Clause #25 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (X1 X2 : Iota), Eq (join a (join X1 X2)) (join (join a X1) X2)) True % 45.57/45.73 Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota), Eq (∀ (X2 : Iota), Eq (join a (join a_1 X2)) (join (join a a_1) X2)) True % 45.57/45.73 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), Eq (Eq (join a (join a_1 a_2)) (join (join a a_1) a_2)) True % 45.57/45.73 Clause #28 (by clausification #[27]): ∀ (a a_1 a_2 : Iota), Eq (join a (join a_1 a_2)) (join (join a a_1) a_2) % 45.57/45.73 Clause #29 (by superposition #[28, 21]): ∀ (a a_1 : Iota), Eq top (join a (join a_1 (complement (join a a_1)))) % 45.57/45.73 Clause #30 (by superposition #[28, 24]): ∀ (a a_1 a_2 : Iota), Eq (join a (join a_1 a_2)) (join a_2 (join a a_1)) % 45.57/45.73 Clause #33 (by superposition #[28, 21]): ∀ (a a_1 : Iota), Eq (join a (join (complement a) a_1)) (join top a_1) % 45.57/45.73 Clause #38 (by superposition #[33, 21]): ∀ (a : Iota), Eq (join a top) (join top (complement (complement a))) % 45.57/45.73 Clause #39 (by superposition #[33, 24]): ∀ (a a_1 : Iota), Eq (join a (join a_1 (complement a))) (join top a_1) % 45.57/45.73 Clause #44 (by superposition #[39, 38]): ∀ (a : Iota), Eq (join (complement a) (join a top)) (join top top) % 45.57/45.73 Clause #51 (by clausification #[2]): ∀ (a : Iota), % 45.57/45.73 Eq % 45.57/45.73 (∀ (X1 : Iota), % 45.57/45.73 Eq a (join (complement (join (complement a) (complement X1))) (complement (join (complement a) X1)))) % 45.57/45.73 True % 45.57/45.73 Clause #52 (by clausification #[51]): ∀ (a a_1 : Iota), % 45.57/45.73 Eq (Eq a (join (complement (join (complement a) (complement a_1))) (complement (join (complement a) a_1)))) True % 45.57/45.75 Clause #53 (by clausification #[52]): ∀ (a a_1 : Iota), Eq a (join (complement (join (complement a) (complement a_1))) (complement (join (complement a) a_1))) % 45.57/45.75 Clause #55 (by superposition #[53, 39]): ∀ (a a_1 : Iota), Eq (join (join (complement a) a_1) a) (join top (complement (join (complement a) (complement a_1)))) % 45.57/45.75 Clause #58 (by superposition #[53, 24]): ∀ (a a_1 : Iota), Eq a (join (complement (join (complement a) a_1)) (complement (join (complement a) (complement a_1)))) % 45.57/45.75 Clause #61 (by superposition #[53, 44]): ∀ (a : Iota), Eq a (join (complement (join (complement a) (complement (join a top)))) (complement (join top top))) % 45.57/45.75 Clause #63 (by superposition #[53, 33]): ∀ (a a_1 : Iota), % 45.57/45.75 Eq a % 45.57/45.75 (join (complement (join (complement a) (complement (join (complement (complement a)) a_1)))) % 45.57/45.75 (complement (join top a_1))) % 45.57/45.75 Clause #65 (by superposition #[53, 24]): ∀ (a a_1 : Iota), Eq a (join (complement (join (complement a) (complement a_1))) (complement (join a_1 (complement a)))) % 45.57/45.75 Clause #81 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (X1 : Iota), Eq (meet a X1) (complement (join (complement a) (complement X1)))) True % 45.57/45.75 Clause #82 (by clausification #[81]): ∀ (a a_1 : Iota), Eq (Eq (meet a a_1) (complement (join (complement a) (complement a_1)))) True % 45.57/45.75 Clause #83 (by clausification #[82]): ∀ (a a_1 : Iota), Eq (meet a a_1) (complement (join (complement a) (complement a_1))) % 45.57/45.75 Clause #94 (by superposition #[83, 21]): ∀ (a : Iota), Eq (meet a (complement a)) (complement top) % 45.57/45.75 Clause #95 (by superposition #[83, 24]): ∀ (a a_1 : Iota), Eq (meet a a_1) (complement (join (complement a_1) (complement a))) % 45.57/45.75 Clause #96 (by superposition #[94, 19]): Eq zero (complement top) % 45.57/45.75 Clause #101 (by superposition #[96, 21]): Eq top (join top zero) % 45.57/45.75 Clause #106 (by superposition #[96, 83]): ∀ (a : Iota), Eq (meet a top) (complement (join (complement a) zero)) % 45.57/45.75 Clause #122 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (X1 X2 : Iota), Eq (composition (join a X1) X2) (join (composition a X2) (composition X1 X2))) True % 45.57/45.75 Clause #123 (by clausification #[122]): ∀ (a a_1 : Iota), % 45.57/45.75 Eq (∀ (X2 : Iota), Eq (composition (join a a_1) X2) (join (composition a X2) (composition a_1 X2))) True % 45.57/45.75 Clause #124 (by clausification #[123]): ∀ (a a_1 a_2 : Iota), Eq (Eq (composition (join a a_1) a_2) (join (composition a a_2) (composition a_1 a_2))) True % 45.57/45.75 Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 : Iota), Eq (composition (join a a_1) a_2) (join (composition a a_2) (composition a_1 a_2)) % 45.57/45.75 Clause #174 (by forward demodulation #[106, 24]): ∀ (a : Iota), Eq (meet a top) (complement (join zero (complement a))) % 45.57/45.75 Clause #187 (by superposition #[174, 21]): Eq (meet zero top) (complement top) % 45.57/45.75 Clause #191 (by forward demodulation #[187, 96]): Eq (meet zero top) zero % 45.57/45.75 Clause #193 (by clausification #[9]): ∀ (a : Iota), Eq (∀ (X1 : Iota), Eq (converse (composition a X1)) (composition (converse X1) (converse a))) True % 45.57/45.75 Clause #194 (by clausification #[193]): ∀ (a a_1 : Iota), Eq (Eq (converse (composition a a_1)) (composition (converse a_1) (converse a))) True % 45.57/45.75 Clause #195 (by clausification #[194]): ∀ (a a_1 : Iota), Eq (converse (composition a a_1)) (composition (converse a_1) (converse a)) % 45.57/45.75 Clause #199 (by superposition #[195, 15]): ∀ (a a_1 : Iota), Eq (converse (composition (converse a) a_1)) (composition (converse a_1) a) % 45.57/45.75 Clause #207 (by clausification #[10]): ∀ (a : Iota), % 45.57/45.75 Eq % 45.57/45.75 (∀ (X1 : Iota), % 45.57/45.75 Eq (join (composition (converse a) (complement (composition a X1))) (complement X1)) (complement X1)) % 45.57/45.75 True % 45.57/45.75 Clause #208 (by clausification #[207]): ∀ (a a_1 : Iota), % 45.57/45.75 Eq (Eq (join (composition (converse a) (complement (composition a a_1))) (complement a_1)) (complement a_1)) True % 45.57/45.75 Clause #209 (by clausification #[208]): ∀ (a a_1 : Iota), % 45.57/45.75 Eq (join (composition (converse a) (complement (composition a a_1))) (complement a_1)) (complement a_1) % 45.57/45.75 Clause #240 (by clausification #[13]): Eq % 45.57/45.75 (∀ (X0 X1 X2 : Iota), % 45.57/45.75 Eq (join (composition (meet X0 (converse X1)) (meet X1 X2)) (composition X0 (meet X1 X2))) % 45.57/45.77 (composition X0 (meet X1 X2))) % 45.57/45.77 False % 45.57/45.77 Clause #241 (by clausification #[240]): ∀ (a : Iota), % 45.57/45.77 Eq % 45.57/45.77 (Not % 45.57/45.77 (∀ (X1 X2 : Iota), % 45.57/45.77 Eq (join (composition (meet (skS.0 0 a) (converse X1)) (meet X1 X2)) (composition (skS.0 0 a) (meet X1 X2))) % 45.57/45.77 (composition (skS.0 0 a) (meet X1 X2)))) % 45.57/45.77 True % 45.57/45.77 Clause #242 (by clausification #[241]): ∀ (a : Iota), % 45.57/45.77 Eq % 45.57/45.77 (∀ (X1 X2 : Iota), % 45.57/45.77 Eq (join (composition (meet (skS.0 0 a) (converse X1)) (meet X1 X2)) (composition (skS.0 0 a) (meet X1 X2))) % 45.57/45.77 (composition (skS.0 0 a) (meet X1 X2))) % 45.57/45.77 False % 45.57/45.77 Clause #243 (by clausification #[242]): ∀ (a a_1 : Iota), % 45.57/45.77 Eq % 45.57/45.77 (Not % 45.57/45.77 (∀ (X2 : Iota), % 45.57/45.77 Eq % 45.57/45.77 (join (composition (meet (skS.0 0 a) (converse (skS.0 1 a a_1))) (meet (skS.0 1 a a_1) X2)) % 45.57/45.77 (composition (skS.0 0 a) (meet (skS.0 1 a a_1) X2))) % 45.57/45.77 (composition (skS.0 0 a) (meet (skS.0 1 a a_1) X2)))) % 45.57/45.77 True % 45.57/45.77 Clause #244 (by clausification #[243]): ∀ (a a_1 : Iota), % 45.57/45.77 Eq % 45.57/45.77 (∀ (X2 : Iota), % 45.57/45.77 Eq % 45.57/45.77 (join (composition (meet (skS.0 0 a) (converse (skS.0 1 a a_1))) (meet (skS.0 1 a a_1) X2)) % 45.57/45.77 (composition (skS.0 0 a) (meet (skS.0 1 a a_1) X2))) % 45.57/45.77 (composition (skS.0 0 a) (meet (skS.0 1 a a_1) X2))) % 45.57/45.77 False % 45.57/45.77 Clause #245 (by clausification #[244]): ∀ (a a_1 a_2 : Iota), % 45.57/45.77 Eq % 45.57/45.77 (Not % 45.57/45.77 (Eq % 45.57/45.77 (join (composition (meet (skS.0 0 a) (converse (skS.0 1 a a_1))) (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 45.57/45.77 (composition (skS.0 0 a) (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 45.57/45.77 (composition (skS.0 0 a) (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))))) % 45.57/45.77 True % 45.57/45.77 Clause #246 (by clausification #[245]): ∀ (a a_1 a_2 : Iota), % 45.57/45.77 Eq % 45.57/45.77 (Eq % 45.57/45.77 (join (composition (meet (skS.0 0 a) (converse (skS.0 1 a a_1))) (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 45.57/45.77 (composition (skS.0 0 a) (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 45.57/45.77 (composition (skS.0 0 a) (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 45.57/45.77 False % 45.57/45.77 Clause #247 (by clausification #[246]): ∀ (a a_1 a_2 : Iota), % 45.57/45.77 Ne % 45.57/45.77 (join (composition (meet (skS.0 0 a) (converse (skS.0 1 a a_1))) (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 45.57/45.77 (composition (skS.0 0 a) (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 45.57/45.77 (composition (skS.0 0 a) (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 45.57/45.77 Clause #248 (by forward demodulation #[247, 125]): ∀ (a a_1 a_2 : Iota), % 45.57/45.77 Ne % 45.57/45.77 (composition (join (meet (skS.0 0 a) (converse (skS.0 1 a a_1))) (skS.0 0 a)) % 45.57/45.77 (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 45.57/45.77 (composition (skS.0 0 a) (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 45.57/45.77 Clause #249 (by forward demodulation #[248, 24]): ∀ (a a_1 a_2 : Iota), % 45.57/45.77 Ne % 45.57/45.77 (composition (join (skS.0 0 a) (meet (skS.0 0 a) (converse (skS.0 1 a a_1)))) % 45.57/45.77 (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 45.57/45.77 (composition (skS.0 0 a) (meet (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 45.57/45.77 Clause #347 (by superposition #[30, 21]): ∀ (a a_1 : Iota), Eq (join a top) (join (complement a_1) (join a a_1)) % 45.57/45.77 Clause #924 (by superposition #[347, 33]): ∀ (a : Iota), Eq (join (complement (complement a)) top) (join top a) % 45.57/45.77 Clause #1463 (by forward demodulation #[55, 28]): ∀ (a a_1 : Iota), Eq (join (complement a) (join a_1 a)) (join top (complement (join (complement a) (complement a_1)))) % 45.57/45.77 Clause #1464 (by forward demodulation #[1463, 347]): ∀ (a a_1 : Iota), Eq (join a top) (join top (complement (join (complement a_1) (complement a)))) % 45.57/45.77 Clause #1465 (by forward demodulation #[1464, 83]): ∀ (a a_1 : Iota), Eq (join a top) (join top (meet a_1 a)) % 45.57/45.77 Clause #1479 (by superposition #[1465, 19]): ∀ (a : Iota), Eq (join (complement a) top) (join top zero) % 45.57/45.77 Clause #1551 (by forward demodulation #[1479, 101]): ∀ (a : Iota), Eq (join (complement a) top) top % 45.57/45.77 Clause #1553 (by superposition #[1551, 924]): ∀ (a : Iota), Eq top (join top a) % 45.57/45.77 Clause #1589 (by superposition #[1553, 29]): ∀ (a : Iota), Eq top (join a top) % 45.57/45.77 Clause #1644 (by forward demodulation #[58, 83]): ∀ (a a_1 : Iota), Eq a (join (complement (join (complement a) a_1)) (meet a a_1)) % 45.69/45.86 Clause #1721 (by forward demodulation #[61, 1589]): ∀ (a : Iota), Eq a (join (complement (join (complement a) (complement (join a top)))) (complement top)) % 45.69/45.86 Clause #1722 (by forward demodulation #[1721, 96]): ∀ (a : Iota), Eq a (join (complement (join (complement a) (complement (join a top)))) zero) % 45.69/45.86 Clause #1723 (by forward demodulation #[1722, 83]): ∀ (a : Iota), Eq a (join (meet a (join a top)) zero) % 45.69/45.86 Clause #1724 (by forward demodulation #[1723, 1589]): ∀ (a : Iota), Eq a (join (meet a top) zero) % 45.69/45.86 Clause #1727 (by superposition #[1724, 24]): ∀ (a : Iota), Eq (join zero (meet a top)) a % 45.69/45.86 Clause #1733 (by superposition #[1724, 191]): Eq zero (join zero zero) % 45.69/45.86 Clause #1740 (by superposition #[1733, 28]): ∀ (a : Iota), Eq (join zero (join zero a)) (join zero a) % 45.69/45.86 Clause #1779 (by forward demodulation #[63, 1553]): ∀ (a a_1 : Iota), % 45.69/45.86 Eq a (join (complement (join (complement a) (complement (join (complement (complement a)) a_1)))) (complement top)) % 45.69/45.86 Clause #1780 (by forward demodulation #[1779, 96]): ∀ (a a_1 : Iota), % 45.69/45.86 Eq a (join (complement (join (complement a) (complement (join (complement (complement a)) a_1)))) zero) % 45.69/45.86 Clause #1781 (by forward demodulation #[1780, 83]): ∀ (a a_1 : Iota), Eq a (join (meet a (join (complement (complement a)) a_1)) zero) % 45.69/45.86 Clause #1832 (by forward demodulation #[65, 83]): ∀ (a a_1 : Iota), Eq a (join (meet a a_1) (complement (join a_1 (complement a)))) % 45.69/45.86 Clause #2535 (by superposition #[95, 1644]): ∀ (a a_1 : Iota), Eq a (join (meet a_1 a) (meet a (complement a_1))) % 45.69/45.86 Clause #2677 (by superposition #[1740, 1727]): ∀ (a : Iota), Eq (join zero a) a % 45.69/45.86 Clause #2680 (by backward demodulation #[2677, 174]): ∀ (a : Iota), Eq (meet a top) (complement (complement a)) % 45.69/45.86 Clause #2683 (by superposition #[2677, 1727]): ∀ (a : Iota), Eq (meet a top) a % 45.69/45.86 Clause #2696 (by superposition #[2677, 24]): ∀ (a : Iota), Eq (join a zero) a % 45.69/45.86 Clause #2829 (by forward demodulation #[2680, 2683]): ∀ (a : Iota), Eq a (complement (complement a)) % 45.69/45.86 Clause #2830 (by backward demodulation #[2829, 1781]): ∀ (a a_1 : Iota), Eq a (join (meet a (join a a_1)) zero) % 45.69/45.86 Clause #3090 (by superposition #[2830, 2696]): ∀ (a a_1 : Iota), Eq a (meet a (join a a_1)) % 45.69/45.86 Clause #3202 (by superposition #[3090, 1832]): ∀ (a a_1 : Iota), Eq (meet a a_1) (meet (meet a a_1) a) % 45.69/45.86 Clause #4297 (by superposition #[199, 17]): ∀ (a : Iota), Eq (converse (converse a)) (composition (converse one) a) % 45.69/45.86 Clause #4299 (by forward demodulation #[4297, 15]): ∀ (a : Iota), Eq a (composition (converse one) a) % 45.69/45.86 Clause #4301 (by superposition #[4299, 209]): ∀ (a : Iota), Eq (join (complement (composition one a)) (complement a)) (complement a) % 45.69/45.86 Clause #4303 (by superposition #[4299, 17]): Eq one (converse one) % 45.69/45.86 Clause #4328 (by backward demodulation #[4303, 4299]): ∀ (a : Iota), Eq a (composition one a) % 45.69/45.86 Clause #14308 (by forward demodulation #[4301, 4328]): ∀ (a : Iota), Eq (join (complement a) (complement a)) (complement a) % 45.69/45.86 Clause #14350 (by superposition #[14308, 2829]): ∀ (a : Iota), Eq (join a a) a % 45.69/45.86 Clause #14395 (by superposition #[14350, 28]): ∀ (a a_1 : Iota), Eq (join a (join a a_1)) (join a a_1) % 45.69/45.86 Clause #15117 (by superposition #[2535, 14395]): ∀ (a a_1 : Iota), Eq (join (meet a a_1) a_1) a_1 % 45.69/45.86 Clause #15279 (by superposition #[15117, 3202]): ∀ (a a_1 : Iota), Eq (join (meet a a_1) a) a % 45.69/45.86 Clause #15315 (by superposition #[15279, 24]): ∀ (a a_1 : Iota), Eq (join a (meet a a_1)) a % 45.69/45.86 Clause #15363 (by backward positive simplify reflect #[15315, 249]): False % 45.69/45.86 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------