%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : DAT119^1 : TPTP v9.2.0. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n025.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:47:11 PM UTC 2025 % Result : Theorem 17.04s 17.27s % Output : Proof 17.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : DAT119^1 : TPTP v9.2.0. Released v7.0.0. % 0.10/0.13 % Command : duper %s % 0.14/0.34 % Computer : n025.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 21:29:08 EDT 2025 % 0.14/0.35 % CPUTime : % 17.04/17.27 SZS status Theorem for theBenchmark.p % 17.04/17.27 SZS output start Proof for theBenchmark.p % 17.04/17.27 Clause #0 (by assumption #[]): Eq (Eq (coindu1018505716length a xsa) (extended_enat2 (suc na))) True % 17.04/17.27 Clause #31 (by assumption #[]): Eq % 17.04/17.27 (∀ (A : Type) (Y : coindu1593790203_llist A), % 17.04/17.27 Ne Y (coindu1598213697e_LNil A) → % 17.04/17.27 Not (∀ (X212 : A) (X222 : coindu1593790203_llist A), Ne Y (coindu1121789889_LCons A X212 X222))) % 17.04/17.27 True % 17.04/17.27 Clause #50 (by assumption #[]): Eq (∀ (A : Type), Eq (coindu1018505716length A (coindu1598213697e_LNil A)) (zero_zero extended_enat)) True % 17.04/17.27 Clause #54 (by assumption #[]): Eq (∀ (N : nat), Eq (extended_the_enat (extended_enat2 N)) N) True % 17.04/17.27 Clause #83 (by assumption #[]): Eq (∀ (M : nat), Ne (zero_zero nat) (suc M)) True % 17.04/17.27 Clause #95 (by assumption #[]): Eq (Eq (zero_zero extended_enat) (extended_enat2 (zero_zero nat))) True % 17.04/17.27 Clause #273 (by assumption #[]): Eq (∀ (X9 : a) (Xs6 : coindu1593790203_llist a), Eq xsa (coindu1121789889_LCons a X9 Xs6) → thesis) True % 17.04/17.27 Clause #274 (by assumption #[]): Eq (Not thesis) True % 17.04/17.27 Clause #275 (by clausification #[274]): Eq thesis False % 17.04/17.27 Clause #276 (by clausification #[273]): ∀ (a_1 : a), Eq (∀ (Xs6 : coindu1593790203_llist a), Eq xsa (coindu1121789889_LCons a a_1 Xs6) → thesis) True % 17.04/17.27 Clause #277 (by clausification #[276]): ∀ (a_1 : a) (a_2 : coindu1593790203_llist a), Eq (Eq xsa (coindu1121789889_LCons a a_1 a_2) → thesis) True % 17.04/17.27 Clause #278 (by clausification #[277]): ∀ (a_1 : a) (a_2 : coindu1593790203_llist a), Or (Eq (Eq xsa (coindu1121789889_LCons a a_1 a_2)) False) (Eq thesis True) % 17.04/17.27 Clause #279 (by clausification #[278]): ∀ (a_1 : a) (a_2 : coindu1593790203_llist a), Or (Eq thesis True) (Ne xsa (coindu1121789889_LCons a a_1 a_2)) % 17.04/17.27 Clause #280 (by forward demodulation #[279, 275]): ∀ (a_1 : a) (a_2 : coindu1593790203_llist a), Or (Eq False True) (Ne xsa (coindu1121789889_LCons a a_1 a_2)) % 17.04/17.27 Clause #281 (by clausification #[280]): ∀ (a_1 : a) (a_2 : coindu1593790203_llist a), Ne xsa (coindu1121789889_LCons a a_1 a_2) % 17.04/17.27 Clause #282 (by clausification #[0]): Eq (coindu1018505716length a xsa) (extended_enat2 (suc na)) % 17.04/17.27 Clause #859 (by clausification #[83]): ∀ (a : nat), Eq (Ne (zero_zero nat) (suc a)) True % 17.04/17.27 Clause #860 (by clausification #[859]): ∀ (a : nat), Ne (zero_zero nat) (suc a) % 17.04/17.27 Clause #942 (by clausification #[54]): ∀ (a : nat), Eq (Eq (extended_the_enat (extended_enat2 a)) a) True % 17.04/17.27 Clause #943 (by clausification #[942]): ∀ (a : nat), Eq (extended_the_enat (extended_enat2 a)) a % 17.04/17.27 Clause #944 (by superposition #[943, 282]): Eq (extended_the_enat (coindu1018505716length a xsa)) (suc na) % 17.04/17.27 Clause #1864 (by clausification #[95]): Eq (zero_zero extended_enat) (extended_enat2 (zero_zero nat)) % 17.04/17.27 Clause #1865 (by superposition #[1864, 943]): Eq (extended_the_enat (zero_zero extended_enat)) (zero_zero nat) % 17.04/17.27 Clause #6176 (by clausification #[31]): ∀ (a : Type), % 17.04/17.27 Eq % 17.04/17.27 (∀ (Y : coindu1593790203_llist a), % 17.04/17.27 Ne Y (coindu1598213697e_LNil a) → % 17.04/17.27 Not (∀ (X212 : a) (X222 : coindu1593790203_llist a), Ne Y (coindu1121789889_LCons a X212 X222))) % 17.04/17.27 True % 17.04/17.27 Clause #6177 (by clausification #[6176]): ∀ (a : Type) (a_1 : coindu1593790203_llist a), % 17.04/17.27 Eq % 17.04/17.27 (Ne a_1 (coindu1598213697e_LNil a) → % 17.04/17.27 Not (∀ (X212 : a) (X222 : coindu1593790203_llist a), Ne a_1 (coindu1121789889_LCons a X212 X222))) % 17.04/17.27 True % 17.04/17.27 Clause #6178 (by clausification #[6177]): ∀ (a : Type) (a_1 : coindu1593790203_llist a), % 17.04/17.27 Or (Eq (Ne a_1 (coindu1598213697e_LNil a)) False) % 17.04/17.27 (Eq (Not (∀ (X212 : a) (X222 : coindu1593790203_llist a), Ne a_1 (coindu1121789889_LCons a X212 X222))) True) % 17.04/17.27 Clause #6179 (by clausification #[6178]): ∀ (a : Type) (a_1 : coindu1593790203_llist a), % 17.04/17.27 Or (Eq (Not (∀ (X212 : a) (X222 : coindu1593790203_llist a), Ne a_1 (coindu1121789889_LCons a X212 X222))) True) % 17.04/17.27 (Eq a_1 (coindu1598213697e_LNil a)) % 17.04/17.27 Clause #6180 (by clausification #[6179]): ∀ (a : Type) (a_1 : coindu1593790203_llist a), % 17.04/17.27 Or (Eq a_1 (coindu1598213697e_LNil a)) % 17.04/17.27 (Eq (∀ (X212 : a) (X222 : coindu1593790203_llist a), Ne a_1 (coindu1121789889_LCons a X212 X222)) False) % 17.04/17.27 Clause #6181 (by clausification #[6180]): ∀ (a : Type) (a_1 : coindu1593790203_llist a) (a_2 : a), % 17.16/17.41 Or (Eq a_1 (coindu1598213697e_LNil a)) % 17.16/17.41 (Eq (Not (∀ (X222 : coindu1593790203_llist a), Ne a_1 (coindu1121789889_LCons a (skS.0 33 a a_1 a_2) X222))) True) % 17.16/17.41 Clause #6182 (by clausification #[6181]): ∀ (a : Type) (a_1 : coindu1593790203_llist a) (a_2 : a), % 17.16/17.41 Or (Eq a_1 (coindu1598213697e_LNil a)) % 17.16/17.41 (Eq (∀ (X222 : coindu1593790203_llist a), Ne a_1 (coindu1121789889_LCons a (skS.0 33 a a_1 a_2) X222)) False) % 17.16/17.41 Clause #6183 (by clausification #[6182]): ∀ (a : Type) (a_1 : coindu1593790203_llist a) (a_2 : a) (a_3 : coindu1593790203_llist a), % 17.16/17.41 Or (Eq a_1 (coindu1598213697e_LNil a)) % 17.16/17.41 (Eq (Not (Ne a_1 (coindu1121789889_LCons a (skS.0 33 a a_1 a_2) (skS.0 34 a a_1 a_2 a_3)))) True) % 17.16/17.41 Clause #6184 (by clausification #[6183]): ∀ (a : Type) (a_1 : coindu1593790203_llist a) (a_2 : a) (a_3 : coindu1593790203_llist a), % 17.16/17.41 Or (Eq a_1 (coindu1598213697e_LNil a)) % 17.16/17.41 (Eq (Ne a_1 (coindu1121789889_LCons a (skS.0 33 a a_1 a_2) (skS.0 34 a a_1 a_2 a_3))) False) % 17.16/17.41 Clause #6185 (by clausification #[6184]): ∀ (a : Type) (a_1 : coindu1593790203_llist a) (a_2 : a) (a_3 : coindu1593790203_llist a), % 17.16/17.41 Or (Eq a_1 (coindu1598213697e_LNil a)) % 17.16/17.41 (Eq a_1 (coindu1121789889_LCons a (skS.0 33 a a_1 a_2) (skS.0 34 a a_1 a_2 a_3))) % 17.16/17.41 Clause #6190 (by superposition #[6185, 281]): ∀ (a_1 : coindu1593790203_llist a), Or (Eq a_1 (coindu1598213697e_LNil a)) (Ne xsa a_1) % 17.16/17.41 Clause #6351 (by destructive equality resolution #[6190]): Eq xsa (coindu1598213697e_LNil a) % 17.16/17.41 Clause #7011 (by clausification #[50]): ∀ (a : Type), Eq (Eq (coindu1018505716length a (coindu1598213697e_LNil a)) (zero_zero extended_enat)) True % 17.16/17.41 Clause #7012 (by clausification #[7011]): ∀ (a : Type), Eq (coindu1018505716length a (coindu1598213697e_LNil a)) (zero_zero extended_enat) % 17.16/17.41 Clause #7014 (by superposition #[7012, 6351]): Eq (coindu1018505716length a xsa) (zero_zero extended_enat) % 17.16/17.41 Clause #7062 (by backward demodulation #[7014, 944]): Eq (extended_the_enat (zero_zero extended_enat)) (suc na) % 17.16/17.41 Clause #7107 (by superposition #[7062, 1865]): Eq (suc na) (zero_zero nat) % 17.16/17.41 Clause #7161 (by forward contextual literal cutting #[7107, 860]): False % 17.16/17.41 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------