%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : DAT121^1 : TPTP v9.2.0. Released v7.0.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:47:11 PM UTC 2025 % Result : Theorem 12.91s 13.09s % Output : Proof 12.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : DAT121^1 : TPTP v9.2.0. Released v7.0.0. % 0.04/0.13 % Command : duper %s % 0.14/0.34 % Computer : n018.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 22:01:38 EDT 2025 % 0.14/0.34 % CPUTime : % 12.91/13.09 SZS status Theorem for theBenchmark.p % 12.91/13.09 SZS output start Proof for theBenchmark.p % 12.91/13.09 Clause #4 (by assumption #[]): Eq % 12.91/13.09 (∀ (A : Type) (N : extended_enat) (Xs : coindu1593790203_llist A), % 12.91/13.09 Eq (coindu335574135_lnull A (coindu191418589_ldrop A N Xs)) % 12.91/13.09 (ord_less_eq extended_enat (coindu1018505716length A Xs) N)) % 12.91/13.09 True % 12.91/13.09 Clause #21 (by assumption #[]): Eq % 12.91/13.09 (∀ (A : Type) (Llist2 : coindu1593790203_llist A), % 12.91/13.09 coindu335574135_lnull A Llist2 → Eq Llist2 (coindu1598213697e_LNil A)) % 12.91/13.09 True % 12.91/13.09 Clause #333 (by assumption #[]): Eq (ord_less_eq extended_enat (coindu1018505716length a xs) m) True % 12.91/13.09 Clause #334 (by assumption #[]): Eq (Not (Eq (coindu191418589_ldrop a m xs) (coindu1598213697e_LNil a))) True % 12.91/13.09 Clause #367 (by clausification #[4]): ∀ (a : Type), % 12.91/13.09 Eq % 12.91/13.09 (∀ (N : extended_enat) (Xs : coindu1593790203_llist a), % 12.91/13.09 Eq (coindu335574135_lnull a (coindu191418589_ldrop a N Xs)) % 12.91/13.09 (ord_less_eq extended_enat (coindu1018505716length a Xs) N)) % 12.91/13.09 True % 12.91/13.09 Clause #368 (by clausification #[367]): ∀ (a : Type) (a_1 : extended_enat), % 12.91/13.09 Eq % 12.91/13.09 (∀ (Xs : coindu1593790203_llist a), % 12.91/13.09 Eq (coindu335574135_lnull a (coindu191418589_ldrop a a_1 Xs)) % 12.91/13.09 (ord_less_eq extended_enat (coindu1018505716length a Xs) a_1)) % 12.91/13.09 True % 12.91/13.09 Clause #369 (by clausification #[368]): ∀ (a : Type) (a_1 : extended_enat) (a_2 : coindu1593790203_llist a), % 12.91/13.09 Eq % 12.91/13.09 (Eq (coindu335574135_lnull a (coindu191418589_ldrop a a_1 a_2)) % 12.91/13.09 (ord_less_eq extended_enat (coindu1018505716length a a_2) a_1)) % 12.91/13.09 True % 12.91/13.09 Clause #370 (by clausification #[369]): ∀ (a : Type) (a_1 : extended_enat) (a_2 : coindu1593790203_llist a), % 12.91/13.09 Eq (coindu335574135_lnull a (coindu191418589_ldrop a a_1 a_2)) % 12.91/13.09 (ord_less_eq extended_enat (coindu1018505716length a a_2) a_1) % 12.91/13.09 Clause #1091 (by superposition #[333, 370]): Eq (coindu335574135_lnull a (coindu191418589_ldrop a m xs)) True % 12.91/13.09 Clause #1158 (by clausification #[21]): ∀ (a : Type), % 12.91/13.09 Eq (∀ (Llist2 : coindu1593790203_llist a), coindu335574135_lnull a Llist2 → Eq Llist2 (coindu1598213697e_LNil a)) True % 12.91/13.09 Clause #1159 (by clausification #[1158]): ∀ (a : Type) (a_1 : coindu1593790203_llist a), Eq (coindu335574135_lnull a a_1 → Eq a_1 (coindu1598213697e_LNil a)) True % 12.91/13.09 Clause #1160 (by clausification #[1159]): ∀ (a : Type) (a_1 : coindu1593790203_llist a), % 12.91/13.09 Or (Eq (coindu335574135_lnull a a_1) False) (Eq (Eq a_1 (coindu1598213697e_LNil a)) True) % 12.91/13.09 Clause #1161 (by clausification #[1160]): ∀ (a : Type) (a_1 : coindu1593790203_llist a), % 12.91/13.09 Or (Eq (coindu335574135_lnull a a_1) False) (Eq a_1 (coindu1598213697e_LNil a)) % 12.91/13.09 Clause #1162 (by superposition #[1161, 1091]): Or (Eq (coindu191418589_ldrop a m xs) (coindu1598213697e_LNil a)) (Eq False True) % 12.91/13.09 Clause #1168 (by clausification #[1162]): Eq (coindu191418589_ldrop a m xs) (coindu1598213697e_LNil a) % 12.91/13.09 Clause #5416 (by clausification #[334]): Eq (Eq (coindu191418589_ldrop a m xs) (coindu1598213697e_LNil a)) False % 12.91/13.09 Clause #5417 (by clausification #[5416]): Ne (coindu191418589_ldrop a m xs) (coindu1598213697e_LNil a) % 12.91/13.09 Clause #5418 (by forward demodulation #[5417, 1168]): Ne (coindu1598213697e_LNil a) (coindu1598213697e_LNil a) % 12.91/13.09 Clause #5419 (by eliminate resolved literals #[5418]): False % 12.91/13.09 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------