%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SET790+4 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n003.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:30 PM UTC 2025 % Result : Theorem 101.65s 101.85s % Output : Proof 102.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SET790+4 : TPTP v9.2.0. Released v3.2.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n003.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 14:00:23 EDT 2025 % 0.13/0.34 % CPUTime : % 101.65/101.85 SZS status Theorem for theBenchmark.p % 101.65/101.85 SZS output start Proof for theBenchmark.p % 101.65/101.85 Clause #0 (by assumption #[]): Eq % 101.65/101.85 (∀ (R E : Iota), % 101.65/101.85 Iff (order R E) % 101.65/101.85 (And % 101.65/101.85 (And (∀ (X : Iota), member X E → apply R X X) % 101.65/101.85 (∀ (X Y : Iota), And (member X E) (member Y E) → And (apply R X Y) (apply R Y X) → Eq X Y)) % 101.65/101.85 (∀ (X Y Z : Iota), % 101.65/101.85 And (And (member X E) (member Y E)) (member Z E) → And (apply R X Y) (apply R Y Z) → apply R X Z))) % 101.65/101.85 True % 101.65/101.85 Clause #5 (by assumption #[]): Eq (∀ (R E M : Iota), Iff (least M R E) (And (member M E) (∀ (X : Iota), member X E → apply R M X))) True % 101.65/101.85 Clause #10 (by assumption #[]): Eq (Not (∀ (R E M : Iota), And (order R E) (least M R E) → ∀ (X : Iota), least X R E → Eq M X)) True % 101.65/101.85 Clause #11 (by clausification #[10]): Eq (∀ (R E M : Iota), And (order R E) (least M R E) → ∀ (X : Iota), least X R E → Eq M X) False % 101.65/101.85 Clause #12 (by clausification #[11]): ∀ (a : Iota), % 101.65/101.85 Eq % 101.65/101.85 (Not % 101.65/101.85 (∀ (E M : Iota), % 101.65/101.85 And (order (skS.0 0 a) E) (least M (skS.0 0 a) E) → ∀ (X : Iota), least X (skS.0 0 a) E → Eq M X)) % 101.65/101.85 True % 101.65/101.85 Clause #13 (by clausification #[12]): ∀ (a : Iota), % 101.65/101.85 Eq (∀ (E M : Iota), And (order (skS.0 0 a) E) (least M (skS.0 0 a) E) → ∀ (X : Iota), least X (skS.0 0 a) E → Eq M X) % 101.65/101.85 False % 101.65/101.85 Clause #14 (by clausification #[13]): ∀ (a a_1 : Iota), % 101.65/101.85 Eq % 101.65/101.85 (Not % 101.65/101.85 (∀ (M : Iota), % 101.65/101.85 And (order (skS.0 0 a) (skS.0 1 a a_1)) (least M (skS.0 0 a) (skS.0 1 a a_1)) → % 101.65/101.85 ∀ (X : Iota), least X (skS.0 0 a) (skS.0 1 a a_1) → Eq M X)) % 101.65/101.85 True % 101.65/101.85 Clause #15 (by clausification #[14]): ∀ (a a_1 : Iota), % 101.65/101.85 Eq % 101.65/101.85 (∀ (M : Iota), % 101.65/101.85 And (order (skS.0 0 a) (skS.0 1 a a_1)) (least M (skS.0 0 a) (skS.0 1 a a_1)) → % 101.65/101.85 ∀ (X : Iota), least X (skS.0 0 a) (skS.0 1 a a_1) → Eq M X) % 101.65/101.85 False % 101.65/101.85 Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 : Iota), % 101.65/101.85 Eq % 101.65/101.85 (Not % 101.65/101.85 (And (order (skS.0 0 a) (skS.0 1 a a_1)) (least (skS.0 2 a a_1 a_2) (skS.0 0 a) (skS.0 1 a a_1)) → % 101.65/101.85 ∀ (X : Iota), least X (skS.0 0 a) (skS.0 1 a a_1) → Eq (skS.0 2 a a_1 a_2) X)) % 101.65/101.86 True % 101.65/101.86 Clause #17 (by clausification #[16]): ∀ (a a_1 a_2 : Iota), % 101.65/101.86 Eq % 101.65/101.86 (And (order (skS.0 0 a) (skS.0 1 a a_1)) (least (skS.0 2 a a_1 a_2) (skS.0 0 a) (skS.0 1 a a_1)) → % 101.65/101.86 ∀ (X : Iota), least X (skS.0 0 a) (skS.0 1 a a_1) → Eq (skS.0 2 a a_1 a_2) X) % 101.65/101.86 False % 101.65/101.86 Clause #18 (by clausification #[17]): ∀ (a a_1 a_2 : Iota), % 101.65/101.86 Eq (And (order (skS.0 0 a) (skS.0 1 a a_1)) (least (skS.0 2 a a_1 a_2) (skS.0 0 a) (skS.0 1 a a_1))) True % 101.65/101.86 Clause #19 (by clausification #[17]): ∀ (a a_1 a_2 : Iota), Eq (∀ (X : Iota), least X (skS.0 0 a) (skS.0 1 a a_1) → Eq (skS.0 2 a a_1 a_2) X) False % 101.65/101.86 Clause #20 (by clausification #[18]): ∀ (a a_1 a_2 : Iota), Eq (least (skS.0 2 a a_1 a_2) (skS.0 0 a) (skS.0 1 a a_1)) True % 101.65/101.86 Clause #21 (by clausification #[18]): ∀ (a a_1 : Iota), Eq (order (skS.0 0 a) (skS.0 1 a a_1)) True % 101.65/101.86 Clause #44 (by clausification #[0]): ∀ (a : Iota), % 101.65/101.86 Eq % 101.65/101.86 (∀ (E : Iota), % 101.65/101.86 Iff (order a E) % 101.65/101.86 (And % 101.65/101.86 (And (∀ (X : Iota), member X E → apply a X X) % 101.65/101.86 (∀ (X Y : Iota), And (member X E) (member Y E) → And (apply a X Y) (apply a Y X) → Eq X Y)) % 101.65/101.86 (∀ (X Y Z : Iota), % 101.65/101.86 And (And (member X E) (member Y E)) (member Z E) → And (apply a X Y) (apply a Y Z) → apply a X Z))) % 101.65/101.86 True % 101.65/101.86 Clause #45 (by clausification #[44]): ∀ (a a_1 : Iota), % 101.65/101.86 Eq % 101.65/101.86 (Iff (order a a_1) % 101.65/101.86 (And % 101.65/101.86 (And (∀ (X : Iota), member X a_1 → apply a X X) % 101.65/101.86 (∀ (X Y : Iota), And (member X a_1) (member Y a_1) → And (apply a X Y) (apply a Y X) → Eq X Y)) % 101.65/101.86 (∀ (X Y Z : Iota), % 101.65/101.86 And (And (member X a_1) (member Y a_1)) (member Z a_1) → And (apply a X Y) (apply a Y Z) → apply a X Z))) % 101.65/101.86 True % 101.65/101.86 Clause #47 (by clausification #[45]): ∀ (a a_1 : Iota), % 101.65/101.86 Or (Eq (order a a_1) False) % 101.65/101.86 (Eq % 101.65/101.86 (And % 101.65/101.86 (And (∀ (X : Iota), member X a_1 → apply a X X) % 101.65/101.86 (∀ (X Y : Iota), And (member X a_1) (member Y a_1) → And (apply a X Y) (apply a Y X) → Eq X Y)) % 101.65/101.86 (∀ (X Y Z : Iota), % 101.65/101.91 And (And (member X a_1) (member Y a_1)) (member Z a_1) → And (apply a X Y) (apply a Y Z) → apply a X Z)) % 101.65/101.91 True) % 101.65/101.91 Clause #72 (by clausification #[19]): ∀ (a a_1 a_2 a_3 : Iota), % 101.65/101.91 Eq % 101.65/101.91 (Not (least (skS.0 11 a a_1 a_2 a_3) (skS.0 0 a) (skS.0 1 a a_1) → Eq (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3))) % 101.65/101.91 True % 101.65/101.91 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 a_3 : Iota), % 101.65/101.91 Eq (least (skS.0 11 a a_1 a_2 a_3) (skS.0 0 a) (skS.0 1 a a_1) → Eq (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) % 101.65/101.91 False % 101.65/101.91 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 a_3 : Iota), Eq (least (skS.0 11 a a_1 a_2 a_3) (skS.0 0 a) (skS.0 1 a a_1)) True % 101.65/101.91 Clause #75 (by clausification #[73]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Eq (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) False % 101.65/101.91 Clause #136 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (E M : Iota), Iff (least M a E) (And (member M E) (∀ (X : Iota), member X E → apply a M X))) True % 101.65/101.91 Clause #137 (by clausification #[136]): ∀ (a a_1 : Iota), % 101.65/101.91 Eq (∀ (M : Iota), Iff (least M a a_1) (And (member M a_1) (∀ (X : Iota), member X a_1 → apply a M X))) True % 101.65/101.91 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), Eq (Iff (least a a_1 a_2) (And (member a a_2) (∀ (X : Iota), member X a_2 → apply a_1 a X))) True % 101.65/101.91 Clause #140 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), % 101.65/101.91 Or (Eq (least a a_1 a_2) False) (Eq (And (member a a_2) (∀ (X : Iota), member X a_2 → apply a_1 a X)) True) % 101.65/101.91 Clause #151 (by clausification #[140]): ∀ (a a_1 a_2 : Iota), Or (Eq (least a a_1 a_2) False) (Eq (∀ (X : Iota), member X a_2 → apply a_1 a X) True) % 101.65/101.91 Clause #152 (by clausification #[140]): ∀ (a a_1 a_2 : Iota), Or (Eq (least a a_1 a_2) False) (Eq (member a a_2) True) % 101.65/101.91 Clause #153 (by clausification #[151]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (least a a_1 a_2) False) (Eq (member a_3 a_2 → apply a_1 a a_3) True) % 101.65/101.91 Clause #154 (by clausification #[153]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (least a a_1 a_2) False) (Or (Eq (member a_3 a_2) False) (Eq (apply a_1 a a_3) True)) % 101.65/101.91 Clause #155 (by superposition #[154, 20]): ∀ (a a_1 a_2 a_3 : Iota), % 101.65/101.91 Or (Eq (member a (skS.0 1 a_1 a_2)) False) % 101.65/101.91 (Or (Eq (apply (skS.0 0 a_1) (skS.0 2 a_1 a_2 a_3) a) True) (Eq False True)) % 101.65/101.91 Clause #156 (by superposition #[154, 74]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 101.65/101.91 Or (Eq (member a (skS.0 1 a_1 a_2)) False) % 101.65/101.91 (Or (Eq (apply (skS.0 0 a_1) (skS.0 11 a_1 a_2 a_3 a_4) a) True) (Eq False True)) % 101.65/101.91 Clause #172 (by superposition #[152, 20]): ∀ (a a_1 a_2 : Iota), Or (Eq (member (skS.0 2 a a_1 a_2) (skS.0 1 a a_1)) True) (Eq False True) % 101.65/101.91 Clause #173 (by superposition #[152, 74]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (member (skS.0 11 a a_1 a_2 a_3) (skS.0 1 a a_1)) True) (Eq False True) % 101.65/101.91 Clause #238 (by clausification #[172]): ∀ (a a_1 a_2 : Iota), Eq (member (skS.0 2 a a_1 a_2) (skS.0 1 a a_1)) True % 101.65/101.91 Clause #246 (by clausification #[47]): ∀ (a a_1 : Iota), % 101.65/101.91 Or (Eq (order a a_1) False) % 101.65/101.91 (Eq % 101.65/101.91 (And (∀ (X : Iota), member X a_1 → apply a X X) % 101.65/101.91 (∀ (X Y : Iota), And (member X a_1) (member Y a_1) → And (apply a X Y) (apply a Y X) → Eq X Y)) % 101.65/101.91 True) % 101.65/101.91 Clause #256 (by clausification #[246]): ∀ (a a_1 : Iota), % 101.65/101.91 Or (Eq (order a a_1) False) % 101.65/101.91 (Eq (∀ (X Y : Iota), And (member X a_1) (member Y a_1) → And (apply a X Y) (apply a Y X) → Eq X Y) True) % 101.65/101.91 Clause #258 (by clausification #[256]): ∀ (a a_1 a_2 : Iota), % 101.65/101.91 Or (Eq (order a a_1) False) % 101.65/101.91 (Eq (∀ (Y : Iota), And (member a_2 a_1) (member Y a_1) → And (apply a a_2 Y) (apply a Y a_2) → Eq a_2 Y) True) % 101.65/101.91 Clause #259 (by clausification #[258]): ∀ (a a_1 a_2 a_3 : Iota), % 101.65/101.91 Or (Eq (order a a_1) False) % 101.65/101.91 (Eq (And (member a_2 a_1) (member a_3 a_1) → And (apply a a_2 a_3) (apply a a_3 a_2) → Eq a_2 a_3) True) % 101.65/101.91 Clause #260 (by clausification #[259]): ∀ (a a_1 a_2 a_3 : Iota), % 101.65/101.91 Or (Eq (order a a_1) False) % 101.65/101.91 (Or (Eq (And (member a_2 a_1) (member a_3 a_1)) False) % 101.65/101.91 (Eq (And (apply a a_2 a_3) (apply a a_3 a_2) → Eq a_2 a_3) True)) % 101.65/101.91 Clause #261 (by clausification #[260]): ∀ (a a_1 a_2 a_3 : Iota), % 101.74/101.97 Or (Eq (order a a_1) False) % 101.74/101.97 (Or (Eq (And (apply a a_2 a_3) (apply a a_3 a_2) → Eq a_2 a_3) True) % 101.74/101.97 (Or (Eq (member a_2 a_1) False) (Eq (member a_3 a_1) False))) % 101.74/101.97 Clause #262 (by clausification #[261]): ∀ (a a_1 a_2 a_3 : Iota), % 101.74/101.97 Or (Eq (order a a_1) False) % 101.74/101.97 (Or (Eq (member a_2 a_1) False) % 101.74/101.97 (Or (Eq (member a_3 a_1) False) (Or (Eq (And (apply a a_2 a_3) (apply a a_3 a_2)) False) (Eq (Eq a_2 a_3) True)))) % 101.74/101.97 Clause #263 (by clausification #[262]): ∀ (a a_1 a_2 a_3 : Iota), % 101.74/101.97 Or (Eq (order a a_1) False) % 101.74/101.97 (Or (Eq (member a_2 a_1) False) % 101.74/101.97 (Or (Eq (member a_3 a_1) False) % 101.74/101.97 (Or (Eq (Eq a_2 a_3) True) (Or (Eq (apply a a_2 a_3) False) (Eq (apply a a_3 a_2) False))))) % 101.74/101.97 Clause #264 (by clausification #[263]): ∀ (a a_1 a_2 a_3 : Iota), % 101.74/101.97 Or (Eq (order a a_1) False) % 101.74/101.97 (Or (Eq (member a_2 a_1) False) % 101.74/101.97 (Or (Eq (member a_3 a_1) False) (Or (Eq (apply a a_2 a_3) False) (Or (Eq (apply a a_3 a_2) False) (Eq a_2 a_3))))) % 101.74/101.97 Clause #265 (by superposition #[264, 21]): ∀ (a a_1 a_2 a_3 : Iota), % 101.74/101.97 Or (Eq (member a (skS.0 1 a_1 a_2)) False) % 101.74/101.97 (Or (Eq (member a_3 (skS.0 1 a_1 a_2)) False) % 101.74/101.97 (Or (Eq (apply (skS.0 0 a_1) a a_3) False) % 101.74/101.97 (Or (Eq (apply (skS.0 0 a_1) a_3 a) False) (Or (Eq a a_3) (Eq False True))))) % 101.74/101.97 Clause #276 (by clausification #[173]): ∀ (a a_1 a_2 a_3 : Iota), Eq (member (skS.0 11 a a_1 a_2 a_3) (skS.0 1 a a_1)) True % 101.74/101.97 Clause #327 (by clausification #[75]): ∀ (a a_1 a_2 a_3 : Iota), Ne (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3) % 101.74/101.97 Clause #396 (by clausification #[155]): ∀ (a a_1 a_2 a_3 : Iota), % 101.74/101.97 Or (Eq (member a (skS.0 1 a_1 a_2)) False) (Eq (apply (skS.0 0 a_1) (skS.0 2 a_1 a_2 a_3) a) True) % 101.74/101.97 Clause #398 (by superposition #[396, 276]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 101.74/101.97 Or (Eq (apply (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) True) (Eq False True) % 101.74/101.97 Clause #459 (by clausification #[398]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (apply (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) True % 101.74/101.97 Clause #484 (by clausification #[156]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 101.74/101.97 Or (Eq (member a (skS.0 1 a_1 a_2)) False) (Eq (apply (skS.0 0 a_1) (skS.0 11 a_1 a_2 a_3 a_4) a) True) % 101.74/101.97 Clause #485 (by superposition #[484, 238]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 101.74/101.97 Or (Eq (apply (skS.0 0 a) (skS.0 11 a a_1 a_2 a_3) (skS.0 2 a a_1 a_4)) True) (Eq False True) % 101.74/101.97 Clause #539 (by clausification #[485]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (apply (skS.0 0 a) (skS.0 11 a a_1 a_2 a_3) (skS.0 2 a a_1 a_4)) True % 101.74/101.97 Clause #542 (by clausification #[265]): ∀ (a a_1 a_2 a_3 : Iota), % 101.74/101.97 Or (Eq (member a (skS.0 1 a_1 a_2)) False) % 101.74/101.97 (Or (Eq (member a_3 (skS.0 1 a_1 a_2)) False) % 101.74/101.97 (Or (Eq (apply (skS.0 0 a_1) a a_3) False) (Or (Eq (apply (skS.0 0 a_1) a_3 a) False) (Eq a a_3)))) % 101.74/101.97 Clause #543 (by superposition #[542, 238]): ∀ (a a_1 a_2 a_3 : Iota), % 101.74/101.97 Or (Eq (member a (skS.0 1 a_1 a_2)) False) % 101.74/101.97 (Or (Eq (apply (skS.0 0 a_1) (skS.0 2 a_1 a_2 a_3) a) False) % 101.74/101.97 (Or (Eq (apply (skS.0 0 a_1) a (skS.0 2 a_1 a_2 a_3)) False) (Or (Eq (skS.0 2 a_1 a_2 a_3) a) (Eq False True)))) % 101.74/101.97 Clause #1460 (by clausification #[543]): ∀ (a a_1 a_2 a_3 : Iota), % 101.74/101.97 Or (Eq (member a (skS.0 1 a_1 a_2)) False) % 101.74/101.97 (Or (Eq (apply (skS.0 0 a_1) (skS.0 2 a_1 a_2 a_3) a) False) % 101.74/101.97 (Or (Eq (apply (skS.0 0 a_1) a (skS.0 2 a_1 a_2 a_3)) False) (Eq (skS.0 2 a_1 a_2 a_3) a))) % 101.74/101.97 Clause #1462 (by superposition #[1460, 276]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 101.74/101.97 Or (Eq (apply (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) False) % 101.74/101.97 (Or (Eq (apply (skS.0 0 a) (skS.0 11 a a_1 a_3 a_4) (skS.0 2 a a_1 a_2)) False) % 101.74/101.97 (Or (Eq (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) (Eq False True))) % 101.74/101.97 Clause #10351 (by clausification #[1462]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 101.74/101.97 Or (Eq (apply (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) False) % 101.74/101.97 (Or (Eq (apply (skS.0 0 a) (skS.0 11 a a_1 a_3 a_4) (skS.0 2 a a_1 a_2)) False) % 101.74/101.97 (Eq (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4))) % 101.74/101.97 Clause #10352 (by superposition #[10351, 459]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 101.74/101.97 Or (Eq (apply (skS.0 0 a) (skS.0 11 a a_1 a_2 a_3) (skS.0 2 a a_1 a_4)) False) % 102.02/102.21 (Or (Eq (skS.0 2 a a_1 a_4) (skS.0 11 a a_1 a_2 a_3)) (Eq False True)) % 102.02/102.21 Clause #10353 (by clausification #[10352]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 102.02/102.21 Or (Eq (apply (skS.0 0 a) (skS.0 11 a a_1 a_2 a_3) (skS.0 2 a a_1 a_4)) False) % 102.02/102.21 (Eq (skS.0 2 a a_1 a_4) (skS.0 11 a a_1 a_2 a_3)) % 102.02/102.21 Clause #10354 (by superposition #[10353, 539]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) (Eq False True) % 102.02/102.21 Clause #10355 (by clausification #[10354]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) % 102.02/102.21 Clause #10356 (by backward contextual literal cutting #[10355, 327]): False % 102.02/102.21 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------