%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : REL001+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:31 PM UTC 2025 % Result : Theorem 5.74s 5.90s % Output : Proof 5.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : REL001+1 : TPTP v9.2.0. Released v4.0.0. % 0.12/0.14 % Command : duper %s % 0.15/0.35 % Computer : n006.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Thu Oct 2 12:03:23 EDT 2025 % 0.15/0.36 % CPUTime : % 5.74/5.90 SZS status Theorem for theBenchmark.p % 5.74/5.90 SZS output start Proof for theBenchmark.p % 5.74/5.90 Clause #0 (by assumption #[]): Eq (∀ (X0 X1 : Iota), Eq (join X0 X1) (join X1 X0)) True % 5.74/5.90 Clause #1 (by assumption #[]): Eq (∀ (X0 X1 X2 : Iota), Eq (join X0 (join X1 X2)) (join (join X0 X1) X2)) True % 5.74/5.90 Clause #2 (by assumption #[]): Eq % 5.74/5.90 (∀ (X0 X1 : Iota), % 5.74/5.90 Eq X0 (join (complement (join (complement X0) (complement X1))) (complement (join (complement X0) X1)))) % 5.74/5.90 True % 5.74/5.90 Clause #3 (by assumption #[]): Eq (∀ (X0 X1 : Iota), Eq (meet X0 X1) (complement (join (complement X0) (complement X1)))) True % 5.74/5.90 Clause #11 (by assumption #[]): Eq (∀ (X0 : Iota), Eq top (join X0 (complement X0))) True % 5.74/5.90 Clause #12 (by assumption #[]): Eq (∀ (X0 : Iota), Eq zero (meet X0 (complement X0))) True % 5.74/5.90 Clause #13 (by assumption #[]): Eq (Not (∀ (X0 : Iota), Eq (join zero X0) X0)) True % 5.74/5.90 Clause #18 (by clausification #[13]): Eq (∀ (X0 : Iota), Eq (join zero X0) X0) False % 5.74/5.90 Clause #19 (by clausification #[18]): ∀ (a : Iota), Eq (Not (Eq (join zero (skS.0 0 a)) (skS.0 0 a))) True % 5.74/5.90 Clause #20 (by clausification #[19]): ∀ (a : Iota), Eq (Eq (join zero (skS.0 0 a)) (skS.0 0 a)) False % 5.74/5.90 Clause #21 (by clausification #[20]): ∀ (a : Iota), Ne (join zero (skS.0 0 a)) (skS.0 0 a) % 5.74/5.90 Clause #22 (by clausification #[12]): ∀ (a : Iota), Eq (Eq zero (meet a (complement a))) True % 5.74/5.90 Clause #23 (by clausification #[22]): ∀ (a : Iota), Eq zero (meet a (complement a)) % 5.74/5.90 Clause #24 (by clausification #[11]): ∀ (a : Iota), Eq (Eq top (join a (complement a))) True % 5.74/5.90 Clause #25 (by clausification #[24]): ∀ (a : Iota), Eq top (join a (complement a)) % 5.74/5.90 Clause #26 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (X1 : Iota), Eq (join a X1) (join X1 a)) True % 5.74/5.90 Clause #27 (by clausification #[26]): ∀ (a a_1 : Iota), Eq (Eq (join a a_1) (join a_1 a)) True % 5.74/5.90 Clause #28 (by clausification #[27]): ∀ (a a_1 : Iota), Eq (join a a_1) (join a_1 a) % 5.74/5.90 Clause #51 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (X1 X2 : Iota), Eq (join a (join X1 X2)) (join (join a X1) X2)) True % 5.74/5.90 Clause #52 (by clausification #[51]): ∀ (a a_1 : Iota), Eq (∀ (X2 : Iota), Eq (join a (join a_1 X2)) (join (join a a_1) X2)) True % 5.74/5.90 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 : Iota), Eq (Eq (join a (join a_1 a_2)) (join (join a a_1) a_2)) True % 5.74/5.90 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 : Iota), Eq (join a (join a_1 a_2)) (join (join a a_1) a_2) % 5.74/5.90 Clause #55 (by superposition #[54, 25]): ∀ (a a_1 : Iota), Eq top (join a (join a_1 (complement (join a a_1)))) % 5.74/5.90 Clause #57 (by superposition #[54, 28]): ∀ (a a_1 a_2 : Iota), Eq (join a (join a_1 a_2)) (join a_1 (join a_2 a)) % 5.74/5.90 Clause #59 (by superposition #[54, 25]): ∀ (a a_1 : Iota), Eq (join a (join (complement a) a_1)) (join top a_1) % 5.74/5.90 Clause #65 (by clausification #[2]): ∀ (a : Iota), % 5.74/5.90 Eq % 5.74/5.90 (∀ (X1 : Iota), % 5.74/5.90 Eq a (join (complement (join (complement a) (complement X1))) (complement (join (complement a) X1)))) % 5.74/5.90 True % 5.74/5.90 Clause #66 (by clausification #[65]): ∀ (a a_1 : Iota), % 5.74/5.90 Eq (Eq a (join (complement (join (complement a) (complement a_1))) (complement (join (complement a) a_1)))) True % 5.74/5.90 Clause #67 (by clausification #[66]): ∀ (a a_1 : Iota), Eq a (join (complement (join (complement a) (complement a_1))) (complement (join (complement a) a_1))) % 5.74/5.90 Clause #70 (by superposition #[67, 28]): ∀ (a a_1 : Iota), Eq a (join (complement (join (complement a) a_1)) (complement (join (complement a) (complement a_1)))) % 5.74/5.90 Clause #75 (by superposition #[67, 25]): ∀ (a : Iota), Eq a (join (complement top) (complement (join (complement a) (complement a)))) % 5.74/5.90 Clause #85 (by superposition #[55, 25]): ∀ (a : Iota), Eq top (join a (join (complement a) (complement top))) % 5.74/5.90 Clause #93 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (X1 : Iota), Eq (meet a X1) (complement (join (complement a) (complement X1)))) True % 5.74/5.90 Clause #94 (by clausification #[93]): ∀ (a a_1 : Iota), Eq (Eq (meet a a_1) (complement (join (complement a) (complement a_1)))) True % 5.74/5.90 Clause #95 (by clausification #[94]): ∀ (a a_1 : Iota), Eq (meet a a_1) (complement (join (complement a) (complement a_1))) % 5.74/5.91 Clause #103 (by superposition #[95, 25]): ∀ (a : Iota), Eq (meet a (complement a)) (complement top) % 5.74/5.91 Clause #105 (by superposition #[103, 23]): Eq zero (complement top) % 5.74/5.91 Clause #107 (by backward demodulation #[105, 85]): ∀ (a : Iota), Eq top (join a (join (complement a) zero)) % 5.74/5.91 Clause #110 (by superposition #[105, 25]): Eq top (join top zero) % 5.74/5.91 Clause #111 (by superposition #[105, 95]): ∀ (a : Iota), Eq (meet a top) (complement (join (complement a) zero)) % 5.74/5.91 Clause #114 (by superposition #[110, 28]): Eq (join zero top) top % 5.74/5.91 Clause #117 (by superposition #[114, 54]): ∀ (a : Iota), Eq (join zero (join top a)) (join top a) % 5.74/5.91 Clause #132 (by forward demodulation #[107, 28]): ∀ (a : Iota), Eq top (join a (join zero (complement a))) % 5.74/5.91 Clause #309 (by forward demodulation #[111, 28]): ∀ (a : Iota), Eq (meet a top) (complement (join zero (complement a))) % 5.74/5.91 Clause #320 (by superposition #[309, 25]): Eq (meet zero top) (complement top) % 5.74/5.91 Clause #324 (by forward demodulation #[320, 105]): Eq (meet zero top) zero % 5.74/5.91 Clause #332 (by superposition #[117, 28]): ∀ (a : Iota), Eq (join zero (join a top)) (join a top) % 5.74/5.91 Clause #589 (by superposition #[57, 114]): ∀ (a : Iota), Eq (join a top) (join zero (join top a)) % 5.74/5.91 Clause #710 (by superposition #[59, 332]): Eq (join (complement zero) top) (join top top) % 5.74/5.91 Clause #875 (by forward demodulation #[70, 95]): ∀ (a a_1 : Iota), Eq a (join (complement (join (complement a) a_1)) (meet a a_1)) % 5.74/5.91 Clause #886 (by superposition #[875, 324]): Eq zero (join (complement (join (complement zero) top)) zero) % 5.74/5.91 Clause #923 (by forward demodulation #[886, 710]): Eq zero (join (complement (join top top)) zero) % 5.74/5.91 Clause #930 (by superposition #[923, 28]): Eq (join zero (complement (join top top))) zero % 5.74/5.91 Clause #935 (by superposition #[930, 132]): Eq top (join (join top top) zero) % 5.74/5.91 Clause #981 (by superposition #[935, 28]): Eq (join zero (join top top)) top % 5.74/5.91 Clause #987 (by superposition #[981, 589]): Eq (join top top) top % 5.74/5.91 Clause #995 (by backward demodulation #[987, 930]): Eq (join zero (complement top)) zero % 5.74/5.91 Clause #999 (by forward demodulation #[995, 105]): Eq (join zero zero) zero % 5.74/5.91 Clause #1004 (by superposition #[999, 54]): ∀ (a : Iota), Eq (join zero (join zero a)) (join zero a) % 5.74/5.91 Clause #1069 (by forward demodulation #[75, 95]): ∀ (a : Iota), Eq a (join (complement top) (meet a a)) % 5.74/5.91 Clause #1070 (by forward demodulation #[1069, 105]): ∀ (a : Iota), Eq a (join zero (meet a a)) % 5.74/5.91 Clause #1495 (by superposition #[1004, 1070]): ∀ (a : Iota), Eq (join zero a) a % 5.74/5.91 Clause #1501 (by backward contextual literal cutting #[1495, 21]): False % 5.74/5.91 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------