%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : REL015+1 : TPTP v9.2.0. Released v4.0.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:58:34 PM UTC 2025 % Result : Theorem 26.15s 26.37s % Output : Proof 26.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : REL015+1 : TPTP v9.2.0. Released v4.0.0. % 0.12/0.13 % Command : duper %s % 0.13/0.34 % Computer : n019.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 12:08:23 EDT 2025 % 0.19/0.34 % CPUTime : % 26.15/26.37 SZS status Theorem for theBenchmark.p % 26.15/26.37 SZS output start Proof for theBenchmark.p % 26.15/26.37 Clause #0 (by assumption #[]): Eq (∀ (X0 X1 : Iota), Eq (join X0 X1) (join X1 X0)) True % 26.15/26.37 Clause #1 (by assumption #[]): Eq (∀ (X0 X1 X2 : Iota), Eq (join X0 (join X1 X2)) (join (join X0 X1) X2)) True % 26.15/26.37 Clause #2 (by assumption #[]): Eq % 26.15/26.37 (∀ (X0 X1 : Iota), % 26.15/26.37 Eq X0 (join (complement (join (complement X0) (complement X1))) (complement (join (complement X0) X1)))) % 26.15/26.37 True % 26.15/26.37 Clause #3 (by assumption #[]): Eq (∀ (X0 X1 : Iota), Eq (meet X0 X1) (complement (join (complement X0) (complement X1)))) True % 26.15/26.37 Clause #5 (by assumption #[]): Eq (∀ (X0 : Iota), Eq (composition X0 one) X0) True % 26.15/26.37 Clause #6 (by assumption #[]): Eq (∀ (X0 X1 X2 : Iota), Eq (composition (join X0 X1) X2) (join (composition X0 X2) (composition X1 X2))) True % 26.15/26.37 Clause #7 (by assumption #[]): Eq (∀ (X0 : Iota), Eq (converse (converse X0)) X0) True % 26.15/26.37 Clause #9 (by assumption #[]): Eq (∀ (X0 X1 : Iota), Eq (converse (composition X0 X1)) (composition (converse X1) (converse X0))) True % 26.15/26.37 Clause #11 (by assumption #[]): Eq (∀ (X0 : Iota), Eq top (join X0 (complement X0))) True % 26.15/26.37 Clause #12 (by assumption #[]): Eq (∀ (X0 : Iota), Eq zero (meet X0 (complement X0))) True % 26.15/26.37 Clause #13 (by assumption #[]): Eq (Not (Eq (composition top top) top)) True % 26.15/26.37 Clause #14 (by clausification #[13]): Eq (Eq (composition top top) top) False % 26.15/26.37 Clause #15 (by clausification #[14]): Ne (composition top top) top % 26.15/26.37 Clause #16 (by clausification #[7]): ∀ (a : Iota), Eq (Eq (converse (converse a)) a) True % 26.15/26.37 Clause #17 (by clausification #[16]): ∀ (a : Iota), Eq (converse (converse a)) a % 26.15/26.37 Clause #18 (by clausification #[5]): ∀ (a : Iota), Eq (Eq (composition a one) a) True % 26.15/26.37 Clause #19 (by clausification #[18]): ∀ (a : Iota), Eq (composition a one) a % 26.15/26.37 Clause #20 (by clausification #[12]): ∀ (a : Iota), Eq (Eq zero (meet a (complement a))) True % 26.15/26.37 Clause #21 (by clausification #[20]): ∀ (a : Iota), Eq zero (meet a (complement a)) % 26.15/26.37 Clause #22 (by clausification #[11]): ∀ (a : Iota), Eq (Eq top (join a (complement a))) True % 26.15/26.37 Clause #23 (by clausification #[22]): ∀ (a : Iota), Eq top (join a (complement a)) % 26.15/26.37 Clause #24 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (X1 : Iota), Eq (join a X1) (join X1 a)) True % 26.15/26.37 Clause #25 (by clausification #[24]): ∀ (a a_1 : Iota), Eq (Eq (join a a_1) (join a_1 a)) True % 26.15/26.37 Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota), Eq (join a a_1) (join a_1 a) % 26.15/26.37 Clause #27 (by clausification #[9]): ∀ (a : Iota), Eq (∀ (X1 : Iota), Eq (converse (composition a X1)) (composition (converse X1) (converse a))) True % 26.15/26.37 Clause #28 (by clausification #[27]): ∀ (a a_1 : Iota), Eq (Eq (converse (composition a a_1)) (composition (converse a_1) (converse a))) True % 26.15/26.37 Clause #29 (by clausification #[28]): ∀ (a a_1 : Iota), Eq (converse (composition a a_1)) (composition (converse a_1) (converse a)) % 26.15/26.37 Clause #30 (by superposition #[29, 17]): ∀ (a a_1 : Iota), Eq (converse (composition (converse a) a_1)) (composition (converse a_1) a) % 26.15/26.37 Clause #39 (by superposition #[30, 19]): ∀ (a : Iota), Eq (converse (converse a)) (composition (converse one) a) % 26.15/26.37 Clause #40 (by forward demodulation #[39, 17]): ∀ (a : Iota), Eq a (composition (converse one) a) % 26.15/26.37 Clause #42 (by superposition #[40, 19]): Eq one (converse one) % 26.15/26.37 Clause #45 (by backward demodulation #[42, 40]): ∀ (a : Iota), Eq a (composition one a) % 26.15/26.37 Clause #49 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (X1 X2 : Iota), Eq (join a (join X1 X2)) (join (join a X1) X2)) True % 26.15/26.37 Clause #50 (by clausification #[49]): ∀ (a a_1 : Iota), Eq (∀ (X2 : Iota), Eq (join a (join a_1 X2)) (join (join a a_1) X2)) True % 26.15/26.37 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 : Iota), Eq (Eq (join a (join a_1 a_2)) (join (join a a_1) a_2)) True % 26.15/26.37 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 : Iota), Eq (join a (join a_1 a_2)) (join (join a a_1) a_2) % 26.15/26.37 Clause #53 (by superposition #[52, 23]): ∀ (a a_1 : Iota), Eq top (join a (join a_1 (complement (join a a_1)))) % 26.15/26.37 Clause #55 (by superposition #[52, 26]): ∀ (a a_1 a_2 : Iota), Eq (join a (join a_1 a_2)) (join a_1 (join a_2 a)) % 26.15/26.39 Clause #57 (by superposition #[52, 23]): ∀ (a a_1 : Iota), Eq (join a (join (complement a) a_1)) (join top a_1) % 26.15/26.39 Clause #63 (by clausification #[2]): ∀ (a : Iota), % 26.15/26.39 Eq % 26.15/26.39 (∀ (X1 : Iota), % 26.15/26.39 Eq a (join (complement (join (complement a) (complement X1))) (complement (join (complement a) X1)))) % 26.15/26.39 True % 26.15/26.39 Clause #64 (by clausification #[63]): ∀ (a a_1 : Iota), % 26.15/26.39 Eq (Eq a (join (complement (join (complement a) (complement a_1))) (complement (join (complement a) a_1)))) True % 26.15/26.39 Clause #65 (by clausification #[64]): ∀ (a a_1 : Iota), Eq a (join (complement (join (complement a) (complement a_1))) (complement (join (complement a) a_1))) % 26.15/26.39 Clause #68 (by superposition #[65, 26]): ∀ (a a_1 : Iota), Eq a (join (complement (join (complement a) a_1)) (complement (join (complement a) (complement a_1)))) % 26.15/26.39 Clause #72 (by superposition #[65, 26]): ∀ (a a_1 : Iota), Eq a (join (complement (join (complement a) (complement a_1))) (complement (join a_1 (complement a)))) % 26.15/26.39 Clause #83 (by superposition #[53, 23]): ∀ (a : Iota), Eq top (join a (join (complement a) (complement top))) % 26.15/26.39 Clause #91 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (X1 : Iota), Eq (meet a X1) (complement (join (complement a) (complement X1)))) True % 26.15/26.39 Clause #92 (by clausification #[91]): ∀ (a a_1 : Iota), Eq (Eq (meet a a_1) (complement (join (complement a) (complement a_1)))) True % 26.15/26.39 Clause #93 (by clausification #[92]): ∀ (a a_1 : Iota), Eq (meet a a_1) (complement (join (complement a) (complement a_1))) % 26.15/26.39 Clause #97 (by superposition #[93, 23]): ∀ (a a_1 : Iota), Eq top (join (join (complement a) (complement a_1)) (meet a a_1)) % 26.15/26.39 Clause #101 (by superposition #[93, 23]): ∀ (a : Iota), Eq (meet a (complement a)) (complement top) % 26.15/26.39 Clause #103 (by superposition #[101, 21]): Eq zero (complement top) % 26.15/26.39 Clause #105 (by backward demodulation #[103, 83]): ∀ (a : Iota), Eq top (join a (join (complement a) zero)) % 26.15/26.39 Clause #109 (by superposition #[103, 93]): ∀ (a : Iota), Eq (meet a top) (complement (join (complement a) zero)) % 26.15/26.39 Clause #126 (by forward demodulation #[105, 26]): ∀ (a : Iota), Eq top (join a (join zero (complement a))) % 26.15/26.39 Clause #130 (by superposition #[126, 23]): Eq top (join zero top) % 26.15/26.39 Clause #133 (by superposition #[130, 52]): ∀ (a : Iota), Eq (join zero (join top a)) (join top a) % 26.15/26.39 Clause #135 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (X1 X2 : Iota), Eq (composition (join a X1) X2) (join (composition a X2) (composition X1 X2))) True % 26.15/26.39 Clause #136 (by clausification #[135]): ∀ (a a_1 : Iota), % 26.15/26.39 Eq (∀ (X2 : Iota), Eq (composition (join a a_1) X2) (join (composition a X2) (composition a_1 X2))) True % 26.15/26.39 Clause #137 (by clausification #[136]): ∀ (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 % 26.15/26.39 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), Eq (composition (join a a_1) a_2) (join (composition a a_2) (composition a_1 a_2)) % 26.15/26.39 Clause #149 (by superposition #[138, 45]): ∀ (a a_1 : Iota), Eq (composition (join one a) a_1) (join a_1 (composition a a_1)) % 26.15/26.39 Clause #155 (by superposition #[133, 26]): ∀ (a : Iota), Eq (join zero (join a top)) (join a top) % 26.15/26.39 Clause #381 (by forward demodulation #[109, 26]): ∀ (a : Iota), Eq (meet a top) (complement (join zero (complement a))) % 26.15/26.39 Clause #392 (by superposition #[381, 23]): Eq (meet zero top) (complement top) % 26.15/26.39 Clause #396 (by forward demodulation #[392, 103]): Eq (meet zero top) zero % 26.15/26.39 Clause #410 (by superposition #[57, 155]): Eq (join (complement zero) top) (join top top) % 26.15/26.39 Clause #554 (by superposition #[55, 130]): ∀ (a : Iota), Eq (join a top) (join zero (join top a)) % 26.15/26.39 Clause #786 (by forward demodulation #[68, 93]): ∀ (a a_1 : Iota), Eq a (join (complement (join (complement a) a_1)) (meet a a_1)) % 26.15/26.39 Clause #796 (by superposition #[786, 396]): Eq zero (join (complement (join (complement zero) top)) zero) % 26.15/26.39 Clause #824 (by forward demodulation #[796, 410]): Eq zero (join (complement (join top top)) zero) % 26.15/26.39 Clause #831 (by superposition #[824, 26]): Eq (join zero (complement (join top top))) zero % 26.15/26.39 Clause #836 (by superposition #[831, 126]): Eq top (join (join top top) zero) % 26.25/26.45 Clause #846 (by superposition #[836, 26]): Eq (join zero (join top top)) top % 26.25/26.45 Clause #852 (by superposition #[846, 554]): Eq (join top top) top % 26.25/26.45 Clause #861 (by backward demodulation #[852, 831]): Eq (join zero (complement top)) zero % 26.25/26.45 Clause #865 (by forward demodulation #[861, 103]): Eq (join zero zero) zero % 26.25/26.45 Clause #870 (by superposition #[865, 52]): ∀ (a : Iota), Eq (join zero (join zero a)) (join zero a) % 26.25/26.45 Clause #940 (by forward demodulation #[72, 93]): ∀ (a a_1 : Iota), Eq a (join (meet a a_1) (complement (join a_1 (complement a)))) % 26.25/26.45 Clause #954 (by superposition #[940, 23]): ∀ (a : Iota), Eq a (join (meet a a) (complement top)) % 26.25/26.45 Clause #968 (by forward demodulation #[954, 103]): ∀ (a : Iota), Eq a (join (meet a a) zero) % 26.25/26.45 Clause #972 (by superposition #[968, 26]): ∀ (a : Iota), Eq (join zero (meet a a)) a % 26.25/26.45 Clause #2063 (by superposition #[870, 972]): ∀ (a : Iota), Eq (join zero a) a % 26.25/26.45 Clause #2106 (by superposition #[2063, 972]): ∀ (a : Iota), Eq (meet a a) a % 26.25/26.45 Clause #2250 (by superposition #[97, 2106]): ∀ (a : Iota), Eq top (join (join (complement a) (complement a)) a) % 26.25/26.45 Clause #3646 (by superposition #[2250, 26]): ∀ (a : Iota), Eq (join a (join (complement a) (complement a))) top % 26.25/26.45 Clause #3669 (by superposition #[3646, 57]): ∀ (a : Iota), Eq top (join top (complement a)) % 26.25/26.45 Clause #3705 (by superposition #[3669, 53]): ∀ (a : Iota), Eq top (join a top) % 26.25/26.45 Clause #3741 (by superposition #[3705, 149]): ∀ (a : Iota), Eq (composition top a) (join a (composition top a)) % 26.25/26.45 Clause #3743 (by superposition #[3705, 26]): ∀ (a : Iota), Eq (join top a) top % 26.25/26.45 Clause #10419 (by superposition #[3741, 3743]): Eq (composition top top) top % 26.25/26.45 Clause #10422 (by forward contextual literal cutting #[10419, 15]): False % 26.25/26.45 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------