%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWX199+1 : TPTP v9.3.0. Released v9.3.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 : Tue May 5 06:59:09 PM UTC 2026 % Result : Theorem 6.24s 6.46s % Output : Proof 6.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX199+1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.13 % Command : duper %s % 0.15/0.33 % Computer : n003.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Tue May 5 11:12:11 EDT 2026 % 0.15/0.34 % CPUTime : % 6.24/6.46 SZS status Theorem for theBenchmark.p % 6.24/6.46 SZS output start Proof for theBenchmark.p % 6.24/6.46 Clause #0 (by assumption #[]): Eq (∀ (X X2 : Iota), Eq (head (cons X X2)) X) True % 6.24/6.46 Clause #1 (by assumption #[]): Eq (∀ (X X2 : Iota), Eq (tail (cons X X2)) X2) True % 6.24/6.46 Clause #4 (by assumption #[]): Eq (∀ (X : Iota), Ne z (s X)) True % 6.24/6.46 Clause #5 (by assumption #[]): Eq (∀ (Y : Iota), leqNat z Y) True % 6.24/6.46 Clause #7 (by assumption #[]): Eq (∀ (Z M : Iota), Iff (leqNat (s Z) (s M)) (leqNat Z M)) True % 6.24/6.46 Clause #8 (by assumption #[]): Eq (∀ (Y : Iota), Eq (merge nil Y) Y) True % 6.24/6.46 Clause #9 (by assumption #[]): Eq (∀ (Z Xs : Iota), Eq (merge (cons Z Xs) nil) (cons Z Xs)) True % 6.24/6.46 Clause #10 (by assumption #[]): Eq (∀ (Z Xs Y2 Ys : Iota), leqNat Z Y2 → Eq (merge (cons Z Xs) (cons Y2 Ys)) (cons Z (merge Xs (cons Y2 Ys)))) True % 6.24/6.46 Clause #12 (by assumption #[]): Eq % 6.24/6.46 (Not % 6.24/6.46 (Exists fun Xs => % 6.24/6.46 Exists fun Ys => % 6.24/6.46 Exists fun Zs => % 6.24/6.46 Not (Eq (merge Xs Ys) (merge Ys Xs) → Eq (merge Xs Zs) (merge Zs Xs) → Eq (merge Ys Zs) (merge Zs Ys)))) % 6.24/6.46 True % 6.24/6.46 Clause #13 (by clausification #[5]): ∀ (a : Iota), Eq (leqNat z a) True % 6.24/6.46 Clause #16 (by clausification #[4]): ∀ (a : Iota), Eq (Ne z (s a)) True % 6.24/6.46 Clause #17 (by clausification #[16]): ∀ (a : Iota), Ne z (s a) % 6.24/6.46 Clause #20 (by clausification #[8]): ∀ (a : Iota), Eq (Eq (merge nil a) a) True % 6.24/6.46 Clause #21 (by clausification #[20]): ∀ (a : Iota), Eq (merge nil a) a % 6.24/6.46 Clause #22 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (X2 : Iota), Eq (head (cons a X2)) a) True % 6.24/6.46 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), Eq (Eq (head (cons a a_1)) a) True % 6.24/6.46 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), Eq (head (cons a a_1)) a % 6.24/6.46 Clause #28 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (X2 : Iota), Eq (tail (cons a X2)) X2) True % 6.24/6.46 Clause #29 (by clausification #[28]): ∀ (a a_1 : Iota), Eq (Eq (tail (cons a a_1)) a_1) True % 6.24/6.46 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), Eq (tail (cons a a_1)) a_1 % 6.24/6.46 Clause #31 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (M : Iota), Iff (leqNat (s a) (s M)) (leqNat a M)) True % 6.24/6.46 Clause #32 (by clausification #[31]): ∀ (a a_1 : Iota), Eq (Iff (leqNat (s a) (s a_1)) (leqNat a a_1)) True % 6.24/6.46 Clause #33 (by clausification #[32]): ∀ (a a_1 : Iota), Or (Eq (leqNat (s a) (s a_1)) True) (Eq (leqNat a a_1) False) % 6.24/6.46 Clause #35 (by superposition #[33, 13]): ∀ (a : Iota), Or (Eq (leqNat (s z) (s a)) True) (Eq False True) % 6.24/6.46 Clause #36 (by clausification #[35]): ∀ (a : Iota), Eq (leqNat (s z) (s a)) True % 6.24/6.46 Clause #40 (by clausification #[9]): ∀ (a : Iota), Eq (∀ (Xs : Iota), Eq (merge (cons a Xs) nil) (cons a Xs)) True % 6.24/6.46 Clause #41 (by clausification #[40]): ∀ (a a_1 : Iota), Eq (Eq (merge (cons a a_1) nil) (cons a a_1)) True % 6.24/6.46 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), Eq (merge (cons a a_1) nil) (cons a a_1) % 6.24/6.46 Clause #48 (by clausification #[10]): ∀ (a : Iota), % 6.24/6.46 Eq (∀ (Xs Y2 Ys : Iota), leqNat a Y2 → Eq (merge (cons a Xs) (cons Y2 Ys)) (cons a (merge Xs (cons Y2 Ys)))) True % 6.24/6.46 Clause #49 (by clausification #[48]): ∀ (a a_1 : Iota), % 6.24/6.46 Eq (∀ (Y2 Ys : Iota), leqNat a Y2 → Eq (merge (cons a a_1) (cons Y2 Ys)) (cons a (merge a_1 (cons Y2 Ys)))) True % 6.24/6.46 Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 : Iota), % 6.24/6.46 Eq (∀ (Ys : Iota), leqNat a a_1 → Eq (merge (cons a a_2) (cons a_1 Ys)) (cons a (merge a_2 (cons a_1 Ys)))) True % 6.24/6.46 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 a_3 : Iota), % 6.24/6.46 Eq (leqNat a a_1 → Eq (merge (cons a a_2) (cons a_1 a_3)) (cons a (merge a_2 (cons a_1 a_3)))) True % 6.24/6.46 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 a_3 : Iota), % 6.24/6.46 Or (Eq (leqNat a a_1) False) (Eq (Eq (merge (cons a a_2) (cons a_1 a_3)) (cons a (merge a_2 (cons a_1 a_3)))) True) % 6.24/6.46 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 : Iota), % 6.24/6.46 Or (Eq (leqNat a a_1) False) (Eq (merge (cons a a_2) (cons a_1 a_3)) (cons a (merge a_2 (cons a_1 a_3)))) % 6.24/6.46 Clause #54 (by superposition #[53, 36]): ∀ (a a_1 a_2 : Iota), % 6.24/6.46 Or (Eq (merge (cons (s z) a) (cons (s a_1) a_2)) (cons (s z) (merge a (cons (s a_1) a_2)))) (Eq False True) % 6.24/6.46 Clause #57 (by superposition #[53, 13]): ∀ (a a_1 a_2 : Iota), Or (Eq (merge (cons z a) (cons a_1 a_2)) (cons z (merge a (cons a_1 a_2)))) (Eq False True) % 6.24/6.48 Clause #62 (by clausification #[57]): ∀ (a a_1 a_2 : Iota), Eq (merge (cons z a) (cons a_1 a_2)) (cons z (merge a (cons a_1 a_2))) % 6.24/6.48 Clause #80 (by clausification #[54]): ∀ (a a_1 a_2 : Iota), Eq (merge (cons (s z) a) (cons (s a_1) a_2)) (cons (s z) (merge a (cons (s a_1) a_2))) % 6.24/6.48 Clause #86 (by clausification #[12]): Eq % 6.24/6.48 (Exists fun Xs => % 6.24/6.48 Exists fun Ys => % 6.24/6.48 Exists fun Zs => % 6.24/6.48 Not (Eq (merge Xs Ys) (merge Ys Xs) → Eq (merge Xs Zs) (merge Zs Xs) → Eq (merge Ys Zs) (merge Zs Ys))) % 6.24/6.48 False % 6.24/6.48 Clause #87 (by clausification #[86]): ∀ (a : Iota), % 6.24/6.48 Eq % 6.24/6.48 (Exists fun Ys => % 6.24/6.48 Exists fun Zs => % 6.24/6.48 Not (Eq (merge a Ys) (merge Ys a) → Eq (merge a Zs) (merge Zs a) → Eq (merge Ys Zs) (merge Zs Ys))) % 6.24/6.48 False % 6.24/6.48 Clause #88 (by clausification #[87]): ∀ (a a_1 : Iota), % 6.24/6.48 Eq % 6.24/6.48 (Exists fun Zs => % 6.24/6.48 Not (Eq (merge a a_1) (merge a_1 a) → Eq (merge a Zs) (merge Zs a) → Eq (merge a_1 Zs) (merge Zs a_1))) % 6.24/6.48 False % 6.24/6.48 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 : Iota), % 6.24/6.48 Eq (Not (Eq (merge a a_1) (merge a_1 a) → Eq (merge a a_2) (merge a_2 a) → Eq (merge a_1 a_2) (merge a_2 a_1))) False % 6.24/6.48 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 : Iota), % 6.24/6.48 Eq (Eq (merge a a_1) (merge a_1 a) → Eq (merge a a_2) (merge a_2 a) → Eq (merge a_1 a_2) (merge a_2 a_1)) True % 6.24/6.48 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 : Iota), % 6.24/6.48 Or (Eq (Eq (merge a a_1) (merge a_1 a)) False) % 6.24/6.48 (Eq (Eq (merge a a_2) (merge a_2 a) → Eq (merge a_1 a_2) (merge a_2 a_1)) True) % 6.24/6.48 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 : Iota), % 6.24/6.48 Or (Eq (Eq (merge a a_1) (merge a_1 a) → Eq (merge a_2 a_1) (merge a_1 a_2)) True) (Ne (merge a a_2) (merge a_2 a)) % 6.24/6.48 Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 : Iota), % 6.24/6.48 Or (Ne (merge a a_1) (merge a_1 a)) % 6.24/6.48 (Or (Eq (Eq (merge a a_2) (merge a_2 a)) False) (Eq (Eq (merge a_1 a_2) (merge a_2 a_1)) True)) % 6.24/6.48 Clause #94 (by clausification #[93]): ∀ (a a_1 a_2 : Iota), % 6.24/6.48 Or (Ne (merge a a_1) (merge a_1 a)) % 6.24/6.48 (Or (Eq (Eq (merge a_1 a_2) (merge a_2 a_1)) True) (Ne (merge a a_2) (merge a_2 a))) % 6.24/6.48 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 : Iota), % 6.24/6.48 Or (Ne (merge a a_1) (merge a_1 a)) (Or (Ne (merge a a_2) (merge a_2 a)) (Eq (merge a_1 a_2) (merge a_2 a_1))) % 6.24/6.48 Clause #101 (by superposition #[95, 21]): ∀ (a a_1 : Iota), Or (Ne a (merge a nil)) (Or (Ne (merge nil a_1) (merge a_1 nil)) (Eq (merge a a_1) (merge a_1 a))) % 6.24/6.48 Clause #112 (by forward demodulation #[101, 21]): ∀ (a a_1 : Iota), Or (Ne a (merge a nil)) (Or (Ne a_1 (merge a_1 nil)) (Eq (merge a a_1) (merge a_1 a))) % 6.24/6.48 Clause #113 (by superposition #[112, 42]): ∀ (a a_1 a_2 : Iota), % 6.24/6.48 Or (Ne (cons a a_1) (cons a a_1)) (Or (Ne a_2 (merge a_2 nil)) (Eq (merge (cons a a_1) a_2) (merge a_2 (cons a a_1)))) % 6.24/6.48 Clause #133 (by eliminate resolved literals #[113]): ∀ (a a_1 a_2 : Iota), Or (Ne a (merge a nil)) (Eq (merge (cons a_1 a_2) a) (merge a (cons a_1 a_2))) % 6.24/6.48 Clause #134 (by superposition #[133, 42]): ∀ (a a_1 a_2 a_3 : Iota), % 6.24/6.48 Or (Ne (cons a a_1) (cons a a_1)) (Eq (merge (cons a_2 a_3) (cons a a_1)) (merge (cons a a_1) (cons a_2 a_3))) % 6.24/6.48 Clause #143 (by eliminate resolved literals #[134]): ∀ (a a_1 a_2 a_3 : Iota), Eq (merge (cons a a_1) (cons a_2 a_3)) (merge (cons a_2 a_3) (cons a a_1)) % 6.24/6.48 Clause #144 (by superposition #[143, 62]): ∀ (a a_1 a_2 : Iota), Eq (merge (cons a a_1) (cons z a_2)) (cons z (merge a_2 (cons a a_1))) % 6.24/6.48 Clause #146 (by superposition #[143, 80]): ∀ (a a_1 a_2 : Iota), Eq (merge (cons (s a) a_1) (cons (s z) a_2)) (cons (s z) (merge a_2 (cons (s a) a_1))) % 6.24/6.48 Clause #153 (by superposition #[144, 62]): ∀ (a a_1 : Iota), Eq (cons z (merge a (cons z a_1))) (cons z (merge a_1 (cons z a))) % 6.24/6.48 Clause #184 (by superposition #[153, 21]): ∀ (a : Iota), Eq (cons z (merge a (cons z nil))) (cons z (cons z a)) % 6.24/6.48 Clause #201 (by superposition #[184, 30]): ∀ (a : Iota), Eq (tail (cons z (cons z a))) (merge a (cons z nil)) % 6.24/6.48 Clause #222 (by superposition #[201, 30]): ∀ (a : Iota), Eq (merge a (cons z nil)) (cons z a) % 6.24/6.49 Clause #229 (by superposition #[222, 143]): ∀ (a a_1 : Iota), Eq (merge (cons z nil) (cons a a_1)) (cons z (cons a a_1)) % 6.24/6.49 Clause #815 (by superposition #[146, 80]): ∀ (a a_1 : Iota), Eq (cons (s z) (merge a (cons (s z) a_1))) (cons (s z) (merge a_1 (cons (s z) a))) % 6.24/6.49 Clause #864 (by superposition #[815, 21]): ∀ (a : Iota), Eq (cons (s z) (cons (s z) a)) (cons (s z) (merge a (cons (s z) nil))) % 6.24/6.49 Clause #885 (by superposition #[864, 30]): ∀ (a : Iota), Eq (tail (cons (s z) (cons (s z) a))) (merge a (cons (s z) nil)) % 6.24/6.49 Clause #916 (by superposition #[885, 30]): ∀ (a : Iota), Eq (merge a (cons (s z) nil)) (cons (s z) a) % 6.24/6.49 Clause #926 (by superposition #[916, 229]): Eq (cons (s z) (cons z nil)) (cons z (cons (s z) nil)) % 6.24/6.49 Clause #951 (by superposition #[926, 24]): Eq (head (cons z (cons (s z) nil))) (s z) % 6.24/6.49 Clause #976 (by superposition #[951, 24]): Eq (s z) z % 6.24/6.49 Clause #977 (by forward contextual literal cutting #[976, 17]): False % 6.24/6.49 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------