%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP119^2 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n018.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:51:15 PM UTC 2025 % Result : Theorem 93.44s 93.69s % Output : Proof 94.04s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : ITP119^2 : TPTP v9.2.0. Released v7.5.0. % 0.07/0.14 % Command : duper %s % 0.13/0.36 % Computer : n018.cluster.edu % 0.13/0.36 % Model : x86_64 x86_64 % 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.36 % Memory : 8042.1875MB % 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 300 % 0.13/0.36 % DateTime : Thu Oct 2 23:41:53 EDT 2025 % 0.13/0.36 % CPUTime : % 93.44/93.69 SZS status Theorem for theBenchmark.p % 93.44/93.69 SZS output start Proof for theBenchmark.p % 93.44/93.69 Clause #1 (by assumption #[]): Eq (∀ (B2 A2 : a), less B2 A2 → Ne A2 B2) True % 93.44/93.69 Clause #10 (by assumption #[]): Eq (∀ (A2 B2 : a), Eq (inf A2 B2) (inf B2 A2)) True % 93.44/93.69 Clause #13 (by assumption #[]): Eq (∀ (A2 B2 : a), Eq (sup A2 B2) (sup B2 A2)) True % 93.44/93.69 Clause #14 (by assumption #[]): Eq (∀ (B2 A2 C : a), Eq (sup B2 (sup A2 C)) (sup A2 (sup B2 C))) True % 93.44/93.69 Clause #26 (by assumption #[]): Eq (∀ (A2 : a), Eq (inf A2 A2) A2) True % 93.44/93.69 Clause #29 (by assumption #[]): Eq (∀ (A2 : a), Eq (sup A2 A2) A2) True % 93.44/93.69 Clause #38 (by assumption #[]): Eq (∀ (X Y : a), Eq (sup X (inf X Y)) X) True % 93.44/93.69 Clause #228 (by assumption #[]): Eq (Eq b (inf b c)) True % 93.44/93.69 Clause #229 (by assumption #[]): Eq (Eq (inf c (sup b c)) b) True % 93.44/93.69 Clause #230 (by assumption #[]): Eq (Eq a2 (sup b c)) True % 93.44/93.69 Clause #231 (by assumption #[]): Eq (less b (sup b c)) True % 93.44/93.69 Clause #239 (by clausification #[1]): ∀ (a_1 : a), Eq (∀ (A2 : a), less a_1 A2 → Ne A2 a_1) True % 93.44/93.69 Clause #240 (by clausification #[239]): ∀ (a_1 a_2 : a), Eq (less a_1 a_2 → Ne a_2 a_1) True % 93.44/93.69 Clause #241 (by clausification #[240]): ∀ (a_1 a_2 : a), Or (Eq (less a_1 a_2) False) (Eq (Ne a_2 a_1) True) % 93.44/93.69 Clause #242 (by clausification #[241]): ∀ (a_1 a_2 : a), Or (Eq (less a_1 a_2) False) (Ne a_2 a_1) % 93.44/93.69 Clause #243 (by destructive equality resolution #[242]): ∀ (a : a), Eq (less a a) False % 93.44/93.69 Clause #252 (by clausification #[228]): Eq b (inf b c) % 93.44/93.69 Clause #253 (by clausification #[230]): Eq a2 (sup b c) % 93.44/93.69 Clause #254 (by backward demodulation #[253, 231]): Eq (less b a2) True % 93.44/93.69 Clause #1571 (by clausification #[10]): ∀ (a_1 : a), Eq (∀ (B2 : a), Eq (inf a_1 B2) (inf B2 a_1)) True % 93.44/93.69 Clause #1572 (by clausification #[1571]): ∀ (a_1 a_2 : a), Eq (Eq (inf a_1 a_2) (inf a_2 a_1)) True % 93.44/93.69 Clause #1573 (by clausification #[1572]): ∀ (a_1 a_2 : a), Eq (inf a_1 a_2) (inf a_2 a_1) % 93.44/93.69 Clause #1574 (by superposition #[1573, 252]): Eq b (inf c b) % 93.44/93.69 Clause #2124 (by clausification #[13]): ∀ (a_1 : a), Eq (∀ (B2 : a), Eq (sup a_1 B2) (sup B2 a_1)) True % 93.44/93.69 Clause #2125 (by clausification #[2124]): ∀ (a_1 a_2 : a), Eq (Eq (sup a_1 a_2) (sup a_2 a_1)) True % 93.44/93.69 Clause #2126 (by clausification #[2125]): ∀ (a_1 a_2 : a), Eq (sup a_1 a_2) (sup a_2 a_1) % 93.44/93.69 Clause #2127 (by superposition #[2126, 253]): Eq a2 (sup c b) % 93.44/93.69 Clause #2222 (by clausification #[14]): ∀ (a_1 : a), Eq (∀ (A2 C : a), Eq (sup a_1 (sup A2 C)) (sup A2 (sup a_1 C))) True % 93.44/93.69 Clause #2223 (by clausification #[2222]): ∀ (a_1 a_2 : a), Eq (∀ (C : a), Eq (sup a_1 (sup a_2 C)) (sup a_2 (sup a_1 C))) True % 93.44/93.69 Clause #2224 (by clausification #[2223]): ∀ (a_1 a_2 a_3 : a), Eq (Eq (sup a_1 (sup a_2 a_3)) (sup a_2 (sup a_1 a_3))) True % 93.44/93.69 Clause #2225 (by clausification #[2224]): ∀ (a_1 a_2 a_3 : a), Eq (sup a_1 (sup a_2 a_3)) (sup a_2 (sup a_1 a_3)) % 93.44/93.69 Clause #3883 (by clausification #[26]): ∀ (a_1 : a), Eq (Eq (inf a_1 a_1) a_1) True % 93.44/93.69 Clause #3884 (by clausification #[3883]): ∀ (a_1 : a), Eq (inf a_1 a_1) a_1 % 93.44/93.69 Clause #3945 (by clausification #[29]): ∀ (a_1 : a), Eq (Eq (sup a_1 a_1) a_1) True % 93.44/93.69 Clause #3946 (by clausification #[3945]): ∀ (a_1 : a), Eq (sup a_1 a_1) a_1 % 93.44/93.69 Clause #3956 (by superposition #[3946, 2225]): ∀ (a_1 a_2 : a), Eq (sup a_1 (sup a_2 a_1)) (sup a_2 a_1) % 93.44/93.69 Clause #7823 (by clausification #[38]): ∀ (a_1 : a), Eq (∀ (Y : a), Eq (sup a_1 (inf a_1 Y)) a_1) True % 93.44/93.69 Clause #7824 (by clausification #[7823]): ∀ (a_1 a_2 : a), Eq (Eq (sup a_1 (inf a_1 a_2)) a_1) True % 93.44/93.69 Clause #7825 (by clausification #[7824]): ∀ (a_1 a_2 : a), Eq (sup a_1 (inf a_1 a_2)) a_1 % 93.44/93.69 Clause #7844 (by superposition #[7825, 1574]): Eq (sup c b) c % 93.44/93.69 Clause #7926 (by superposition #[7844, 2127]): Eq a2 c % 93.44/93.69 Clause #7934 (by superposition #[7844, 3956]): Eq (sup b c) c % 93.44/93.69 Clause #8015 (by backward demodulation #[7926, 254]): Eq (less b c) True % 93.44/93.69 Clause #25723 (by clausification #[229]): Eq (inf c (sup b c)) b % 93.44/93.69 Clause #25724 (by forward demodulation #[25723, 7934]): Eq (inf c c) b % 93.44/93.69 Clause #25728 (by superposition #[25724, 3884]): Eq b c % 93.44/93.69 Clause #25870 (by backward demodulation #[25728, 8015]): Eq (less c c) True % 93.44/93.69 Clause #26297 (by superposition #[25870, 243]): Eq True False % 94.04/94.22 Clause #26434 (by clausification #[26297]): False % 94.04/94.22 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------