%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SET901+1 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n029.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 08:00:39 PM UTC 2025 % Result : Theorem 4.99s 5.17s % Output : Proof 5.08s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SET901+1 : TPTP v9.2.0. Released v3.2.0. % 0.06/0.13 % Command : duper %s % 0.14/0.34 % Computer : n029.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu Oct 2 13:39:38 EDT 2025 % 0.14/0.35 % CPUTime : % 4.99/5.17 SZS status Theorem for theBenchmark.p % 4.99/5.17 SZS output start Proof for theBenchmark.p % 4.99/5.17 Clause #0 (by assumption #[]): Eq (∀ (A B : Iota), Eq (unordered_pair A B) (unordered_pair B A)) True % 4.99/5.17 Clause #1 (by assumption #[]): Eq (∀ (A : Iota), Iota → subset A A) True % 4.99/5.17 Clause #5 (by assumption #[]): Eq % 4.99/5.17 (Not % 4.99/5.17 (∀ (A B C : Iota), % 4.99/5.17 Iff (subset A (unordered_pair B C)) % 4.99/5.17 (Not (And (And (And (Ne A empty_set) (Ne A (singleton B))) (Ne A (singleton C))) (Ne A (unordered_pair B C)))))) % 4.99/5.17 True % 4.99/5.17 Clause #6 (by assumption #[]): Eq % 4.99/5.17 (∀ (A B C : Iota), % 4.99/5.17 Iff (subset A (unordered_pair B C)) % 4.99/5.17 (Not (And (And (And (Ne A empty_set) (Ne A (singleton B))) (Ne A (singleton C))) (Ne A (unordered_pair B C))))) % 4.99/5.17 True % 4.99/5.17 Clause #9 (by clausification #[1]): ∀ (a : Iota), Eq (Iota → subset a a) True % 4.99/5.17 Clause #10 (by clausification #[9]): ∀ (a : Iota), Iota → Eq (subset a a) True % 4.99/5.17 Clause #13 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B : Iota), Eq (unordered_pair a B) (unordered_pair B a)) True % 4.99/5.17 Clause #14 (by clausification #[13]): ∀ (a a_1 : Iota), Eq (Eq (unordered_pair a a_1) (unordered_pair a_1 a)) True % 4.99/5.17 Clause #15 (by clausification #[14]): ∀ (a a_1 : Iota), Eq (unordered_pair a a_1) (unordered_pair a_1 a) % 4.99/5.17 Clause #16 (by clausification #[5]): Eq % 4.99/5.17 (∀ (A B C : Iota), % 4.99/5.17 Iff (subset A (unordered_pair B C)) % 4.99/5.17 (Not (And (And (And (Ne A empty_set) (Ne A (singleton B))) (Ne A (singleton C))) (Ne A (unordered_pair B C))))) % 4.99/5.17 False % 4.99/5.17 Clause #17 (by clausification #[16]): ∀ (a : Iota), % 4.99/5.17 Eq % 4.99/5.17 (Not % 4.99/5.17 (∀ (B C : Iota), % 4.99/5.17 Iff (subset (skS.0 2 a) (unordered_pair B C)) % 4.99/5.17 (Not % 4.99/5.17 (And (And (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton B))) (Ne (skS.0 2 a) (singleton C))) % 4.99/5.17 (Ne (skS.0 2 a) (unordered_pair B C)))))) % 4.99/5.17 True % 4.99/5.17 Clause #18 (by clausification #[17]): ∀ (a : Iota), % 4.99/5.17 Eq % 4.99/5.17 (∀ (B C : Iota), % 4.99/5.17 Iff (subset (skS.0 2 a) (unordered_pair B C)) % 4.99/5.17 (Not % 4.99/5.17 (And (And (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton B))) (Ne (skS.0 2 a) (singleton C))) % 4.99/5.17 (Ne (skS.0 2 a) (unordered_pair B C))))) % 4.99/5.17 False % 4.99/5.17 Clause #19 (by clausification #[18]): ∀ (a a_1 : Iota), % 4.99/5.17 Eq % 4.99/5.17 (Not % 4.99/5.17 (∀ (C : Iota), % 4.99/5.17 Iff (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) C)) % 4.99/5.17 (Not % 4.99/5.17 (And % 4.99/5.17 (And (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) % 4.99/5.17 (Ne (skS.0 2 a) (singleton C))) % 4.99/5.17 (Ne (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) C)))))) % 4.99/5.17 True % 4.99/5.17 Clause #20 (by clausification #[19]): ∀ (a a_1 : Iota), % 4.99/5.17 Eq % 4.99/5.17 (∀ (C : Iota), % 4.99/5.17 Iff (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) C)) % 4.99/5.17 (Not % 4.99/5.17 (And % 4.99/5.17 (And (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) % 4.99/5.17 (Ne (skS.0 2 a) (singleton C))) % 4.99/5.17 (Ne (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) C))))) % 4.99/5.17 False % 4.99/5.17 Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 : Iota), % 4.99/5.17 Eq % 4.99/5.17 (Not % 4.99/5.17 (Iff (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 4.99/5.17 (Not % 4.99/5.17 (And % 4.99/5.17 (And (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) % 4.99/5.17 (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2)))) % 4.99/5.17 (Ne (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))))))) % 4.99/5.17 True % 4.99/5.17 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 : Iota), % 4.99/5.17 Eq % 4.99/5.17 (Iff (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 4.99/5.17 (Not % 4.99/5.17 (And % 4.99/5.17 (And (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) % 4.99/5.17 (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2)))) % 4.99/5.17 (Ne (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)))))) % 4.99/5.17 False % 4.99/5.17 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 : Iota), % 4.99/5.17 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) % 4.99/5.17 (Eq % 4.99/5.17 (Not % 4.99/5.17 (And % 4.99/5.17 (And (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) % 4.99/5.17 (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2)))) % 4.99/5.19 (Ne (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))))) % 4.99/5.19 False) % 4.99/5.19 Clause #24 (by clausification #[22]): ∀ (a a_1 a_2 : Iota), % 4.99/5.19 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) True) % 4.99/5.19 (Eq % 4.99/5.19 (Not % 4.99/5.19 (And % 4.99/5.19 (And (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) % 4.99/5.19 (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2)))) % 4.99/5.19 (Ne (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))))) % 4.99/5.19 True) % 4.99/5.19 Clause #25 (by clausification #[23]): ∀ (a a_1 a_2 : Iota), % 4.99/5.19 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) % 4.99/5.19 (Eq % 4.99/5.19 (And % 4.99/5.19 (And (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) % 4.99/5.19 (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2)))) % 4.99/5.19 (Ne (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)))) % 4.99/5.19 True) % 4.99/5.19 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), % 4.99/5.19 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) % 4.99/5.19 (Eq (Ne (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) True) % 4.99/5.19 Clause #27 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), % 4.99/5.19 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) % 4.99/5.19 (Eq % 4.99/5.19 (And (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) % 4.99/5.19 (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2)))) % 4.99/5.19 True) % 4.99/5.19 Clause #28 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), % 4.99/5.19 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) % 4.99/5.19 (Ne (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 4.99/5.19 Clause #29 (by clausification #[6]): ∀ (a : Iota), % 4.99/5.19 Eq % 4.99/5.19 (∀ (B C : Iota), % 4.99/5.19 Iff (subset a (unordered_pair B C)) % 4.99/5.19 (Not (And (And (And (Ne a empty_set) (Ne a (singleton B))) (Ne a (singleton C))) (Ne a (unordered_pair B C))))) % 4.99/5.19 True % 4.99/5.19 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), % 4.99/5.19 Eq % 4.99/5.19 (∀ (C : Iota), % 4.99/5.19 Iff (subset a (unordered_pair a_1 C)) % 4.99/5.19 (Not % 4.99/5.19 (And (And (And (Ne a empty_set) (Ne a (singleton a_1))) (Ne a (singleton C))) (Ne a (unordered_pair a_1 C))))) % 4.99/5.19 True % 4.99/5.19 Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 : Iota), % 4.99/5.19 Eq % 4.99/5.19 (Iff (subset a (unordered_pair a_1 a_2)) % 4.99/5.19 (Not % 4.99/5.19 (And (And (And (Ne a empty_set) (Ne a (singleton a_1))) (Ne a (singleton a_2))) % 4.99/5.19 (Ne a (unordered_pair a_1 a_2))))) % 4.99/5.19 True % 4.99/5.19 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 : Iota), % 4.99/5.19 Or (Eq (subset a (unordered_pair a_1 a_2)) True) % 4.99/5.19 (Eq % 4.99/5.19 (Not % 4.99/5.19 (And (And (And (Ne a empty_set) (Ne a (singleton a_1))) (Ne a (singleton a_2))) % 4.99/5.19 (Ne a (unordered_pair a_1 a_2)))) % 4.99/5.19 False) % 4.99/5.19 Clause #33 (by clausification #[31]): ∀ (a a_1 a_2 : Iota), % 4.99/5.19 Or (Eq (subset a (unordered_pair a_1 a_2)) False) % 4.99/5.19 (Eq % 4.99/5.19 (Not % 4.99/5.19 (And (And (And (Ne a empty_set) (Ne a (singleton a_1))) (Ne a (singleton a_2))) % 4.99/5.19 (Ne a (unordered_pair a_1 a_2)))) % 4.99/5.19 True) % 4.99/5.19 Clause #34 (by clausification #[32]): ∀ (a a_1 a_2 : Iota), % 4.99/5.19 Or (Eq (subset a (unordered_pair a_1 a_2)) True) % 4.99/5.19 (Eq (And (And (And (Ne a empty_set) (Ne a (singleton a_1))) (Ne a (singleton a_2))) (Ne a (unordered_pair a_1 a_2))) % 4.99/5.19 True) % 4.99/5.19 Clause #36 (by clausification #[34]): ∀ (a a_1 a_2 : Iota), % 4.99/5.19 Or (Eq (subset a (unordered_pair a_1 a_2)) True) % 4.99/5.19 (Eq (And (And (Ne a empty_set) (Ne a (singleton a_1))) (Ne a (singleton a_2))) True) % 4.99/5.19 Clause #39 (by clausification #[36]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a (unordered_pair a_1 a_2)) True) (Eq (Ne a (singleton a_2)) True) % 4.99/5.19 Clause #40 (by clausification #[36]): ∀ (a a_1 a_2 : Iota), % 4.99/5.19 Or (Eq (subset a (unordered_pair a_1 a_2)) True) (Eq (And (Ne a empty_set) (Ne a (singleton a_1))) True) % 4.99/5.19 Clause #41 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a (unordered_pair a_1 a_2)) True) (Ne a (singleton a_2)) % 4.99/5.19 Clause #42 (by destructive equality resolution #[41]): ∀ (a a_1 : Iota), Eq (subset (singleton a) (unordered_pair a_1 a)) True % 4.99/5.22 Clause #43 (by superposition #[42, 15]): ∀ (a a_1 : Iota), Eq (subset (singleton a) (unordered_pair a a_1)) True % 4.99/5.22 Clause #45 (by clausification #[40]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a (unordered_pair a_1 a_2)) True) (Eq (Ne a empty_set) True) % 4.99/5.22 Clause #47 (by clausification #[45]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a (unordered_pair a_1 a_2)) True) (Ne a empty_set) % 4.99/5.22 Clause #48 (by destructive equality resolution #[47]): ∀ (a a_1 : Iota), Eq (subset empty_set (unordered_pair a a_1)) True % 4.99/5.22 Clause #49 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), % 4.99/5.22 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) True) % 4.99/5.22 (Eq % 4.99/5.22 (And % 4.99/5.22 (And (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) % 4.99/5.22 (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2)))) % 4.99/5.22 (Ne (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)))) % 4.99/5.22 False) % 4.99/5.22 Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 : Iota), % 4.99/5.22 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) True) % 4.99/5.22 (Or % 4.99/5.22 (Eq % 4.99/5.22 (And (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) % 4.99/5.22 (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2)))) % 4.99/5.22 False) % 4.99/5.22 (Eq (Ne (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False)) % 4.99/5.22 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 : Iota), % 4.99/5.22 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) True) % 4.99/5.22 (Or (Eq (Ne (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) % 4.99/5.22 (Or (Eq (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) False) % 4.99/5.22 (Eq (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) False))) % 4.99/5.22 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 : Iota), % 4.99/5.22 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) True) % 4.99/5.22 (Or (Eq (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) False) % 4.99/5.22 (Or (Eq (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) False) % 4.99/5.22 (Eq (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))))) % 4.99/5.22 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 : Iota), % 4.99/5.22 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) True) % 4.99/5.22 (Or (Eq (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) False) % 4.99/5.22 (Or (Eq (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 4.99/5.22 (Or (Eq (Ne (skS.0 2 a) empty_set) False) (Eq (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1))) False)))) % 4.99/5.22 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 : Iota), % 4.99/5.22 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) True) % 4.99/5.22 (Or (Eq (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 4.99/5.22 (Or (Eq (Ne (skS.0 2 a) empty_set) False) % 4.99/5.22 (Or (Eq (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1))) False) (Eq (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2)))))) % 4.99/5.22 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 : Iota), % 4.99/5.22 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) True) % 4.99/5.22 (Or (Eq (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 4.99/5.22 (Or (Eq (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1))) False) % 4.99/5.22 (Or (Eq (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) (Eq (skS.0 2 a) empty_set)))) % 4.99/5.22 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 : Iota), % 4.99/5.22 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) True) % 4.99/5.22 (Or (Eq (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 4.99/5.22 (Or (Eq (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) % 4.99/5.22 (Or (Eq (skS.0 2 a) empty_set) (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1)))))) % 4.99/5.22 Clause #58 (by clausification #[33]): ∀ (a a_1 a_2 : Iota), % 4.99/5.22 Or (Eq (subset a (unordered_pair a_1 a_2)) False) % 4.99/5.22 (Eq (And (And (And (Ne a empty_set) (Ne a (singleton a_1))) (Ne a (singleton a_2))) (Ne a (unordered_pair a_1 a_2))) % 4.99/5.22 False) % 4.99/5.22 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 : Iota), % 4.99/5.22 Or (Eq (subset a (unordered_pair a_1 a_2)) False) % 5.08/5.25 (Or (Eq (And (And (Ne a empty_set) (Ne a (singleton a_1))) (Ne a (singleton a_2))) False) % 5.08/5.25 (Eq (Ne a (unordered_pair a_1 a_2)) False)) % 5.08/5.25 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset a (unordered_pair a_1 a_2)) False) % 5.08/5.25 (Or (Eq (Ne a (unordered_pair a_1 a_2)) False) % 5.08/5.25 (Or (Eq (And (Ne a empty_set) (Ne a (singleton a_1))) False) (Eq (Ne a (singleton a_2)) False))) % 5.08/5.25 Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset a (unordered_pair a_1 a_2)) False) % 5.08/5.25 (Or (Eq (And (Ne a empty_set) (Ne a (singleton a_1))) False) % 5.08/5.25 (Or (Eq (Ne a (singleton a_2)) False) (Eq a (unordered_pair a_1 a_2)))) % 5.08/5.25 Clause #62 (by clausification #[61]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset a (unordered_pair a_1 a_2)) False) % 5.08/5.25 (Or (Eq (Ne a (singleton a_2)) False) % 5.08/5.25 (Or (Eq a (unordered_pair a_1 a_2)) (Or (Eq (Ne a empty_set) False) (Eq (Ne a (singleton a_1)) False)))) % 5.08/5.25 Clause #63 (by clausification #[62]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset a (unordered_pair a_1 a_2)) False) % 5.08/5.25 (Or (Eq a (unordered_pair a_1 a_2)) % 5.08/5.25 (Or (Eq (Ne a empty_set) False) (Or (Eq (Ne a (singleton a_1)) False) (Eq a (singleton a_2))))) % 5.08/5.25 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset a (unordered_pair a_1 a_2)) False) % 5.08/5.25 (Or (Eq a (unordered_pair a_1 a_2)) % 5.08/5.25 (Or (Eq (Ne a (singleton a_1)) False) (Or (Eq a (singleton a_2)) (Eq a empty_set)))) % 5.08/5.25 Clause #65 (by clausification #[64]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset a (unordered_pair a_1 a_2)) False) % 5.08/5.25 (Or (Eq a (unordered_pair a_1 a_2)) (Or (Eq a (singleton a_2)) (Or (Eq a empty_set) (Eq a (singleton a_1))))) % 5.08/5.25 Clause #69 (by superposition #[65, 56]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 5.08/5.25 (Or (Eq (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) % 5.08/5.25 (Or (Eq (skS.0 2 a) empty_set) % 5.08/5.25 (Or (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1))) % 5.08/5.25 (Or (Eq False True) % 5.08/5.25 (Or (Eq (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 5.08/5.25 (Or (Eq (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) % 5.08/5.25 (Or (Eq (skS.0 2 a) empty_set) (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1)))))))))) % 5.08/5.25 Clause #80 (by clausification #[27]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) % 5.08/5.25 (Eq (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) True) % 5.08/5.25 Clause #81 (by clausification #[27]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) % 5.08/5.25 (Eq (And (Ne (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) True) % 5.08/5.25 Clause #82 (by clausification #[80]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) % 5.08/5.25 (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) % 5.08/5.25 Clause #90 (by clausification #[81]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) % 5.08/5.25 (Eq (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1))) True) % 5.08/5.25 Clause #91 (by clausification #[81]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) % 5.08/5.25 (Eq (Ne (skS.0 2 a) empty_set) True) % 5.08/5.25 Clause #92 (by clausification #[90]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) % 5.08/5.25 (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1))) % 5.08/5.25 Clause #94 (by clausification #[91]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False) (Ne (skS.0 2 a) empty_set) % 5.08/5.25 Clause #99 (by clausification #[69]): ∀ (a a_1 a_2 : Iota), % 5.08/5.25 Or (Eq (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 5.08/5.25 (Or (Eq (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) % 5.08/5.25 (Or (Eq (skS.0 2 a) empty_set) % 5.08/5.25 (Or (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1))) % 5.08/5.25 (Or (Eq (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 5.08/5.25 (Or (Eq (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) % 5.08/5.27 (Or (Eq (skS.0 2 a) empty_set) (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1))))))))) % 5.08/5.27 Clause #100 (by eliminate duplicate literals #[99]): ∀ (a a_1 a_2 : Iota), % 5.08/5.27 Or (Eq (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 5.08/5.27 (Or (Eq (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) % 5.08/5.27 (Or (Eq (skS.0 2 a) empty_set) (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1))))) % 5.08/5.27 Clause #101 (by superposition #[100, 28]): ∀ (a a_1 a_2 : Iota), % 5.08/5.27 Or (Eq (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) % 5.08/5.27 (Or (Eq (skS.0 2 a) empty_set) % 5.08/5.27 (Or (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1))) % 5.08/5.27 (Or (Eq (subset (skS.0 2 a) (skS.0 2 a)) False) (Ne (skS.0 2 a) (skS.0 2 a))))) % 5.08/5.27 Clause #131 (by eliminate resolved literals #[101]): ∀ (a a_1 a_2 : Iota), % 5.08/5.27 Or (Eq (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) % 5.08/5.27 (Or (Eq (skS.0 2 a) empty_set) % 5.08/5.27 (Or (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1))) (Eq (subset (skS.0 2 a) (skS.0 2 a)) False))) % 5.08/5.27 Clause #132 (by superposition #[131, 10]): ∀ (a a_1 a_2 : Iota), % 5.08/5.27 Or (Eq (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) % 5.08/5.27 (Or (Eq (skS.0 2 a) empty_set) (Or (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1))) (Eq False True))) % 5.08/5.27 Clause #134 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), % 5.08/5.27 Or (Eq (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))) % 5.08/5.27 (Or (Eq (skS.0 2 a) empty_set) (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1)))) % 5.08/5.27 Clause #135 (by superposition #[134, 42]): ∀ (a a_1 a_2 a_3 : Iota), % 5.08/5.27 Or (Eq (skS.0 2 a) empty_set) % 5.08/5.27 (Or (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1))) % 5.08/5.27 (Eq (subset (skS.0 2 a) (unordered_pair a_2 (skS.0 4 a a_1 a_3))) True)) % 5.08/5.27 Clause #138 (by superposition #[135, 82]): ∀ (a a_1 a_2 : Iota), % 5.08/5.27 Or (Eq (skS.0 2 a) empty_set) % 5.08/5.27 (Or (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1))) % 5.08/5.27 (Or (Eq True False) (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2))))) % 5.08/5.27 Clause #143 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), % 5.08/5.27 Or (Eq (skS.0 2 a) empty_set) % 5.08/5.27 (Or (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1))) (Ne (skS.0 2 a) (singleton (skS.0 4 a a_1 a_2)))) % 5.08/5.27 Clause #144 (by forward contextual literal cutting #[143, 134]): ∀ (a a_1 : Iota), Or (Eq (skS.0 2 a) empty_set) (Eq (skS.0 2 a) (singleton (skS.0 3 a a_1))) % 5.08/5.27 Clause #146 (by superposition #[144, 43]): ∀ (a a_1 a_2 : Iota), Or (Eq (skS.0 2 a) empty_set) (Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) a_2)) True) % 5.08/5.27 Clause #149 (by superposition #[146, 92]): ∀ (a a_1 : Iota), Or (Eq (skS.0 2 a) empty_set) (Or (Eq True False) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1)))) % 5.08/5.27 Clause #152 (by clausification #[149]): ∀ (a a_1 : Iota), Or (Eq (skS.0 2 a) empty_set) (Ne (skS.0 2 a) (singleton (skS.0 3 a a_1))) % 5.08/5.27 Clause #153 (by forward contextual literal cutting #[152, 144]): ∀ (a : Iota), Eq (skS.0 2 a) empty_set % 5.08/5.27 Clause #161 (by backward contextual literal cutting #[153, 94]): ∀ (a a_1 a_2 : Iota), Eq (subset (skS.0 2 a) (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False % 5.08/5.27 Clause #165 (by forward demodulation #[161, 153]): ∀ (a a_1 a_2 : Iota), Eq (subset empty_set (unordered_pair (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) False % 5.08/5.27 Clause #166 (by superposition #[165, 48]): Eq False True % 5.08/5.27 Clause #167 (by clausification #[166]): False % 5.08/5.27 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------