%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP105^1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n010.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:51:13 PM UTC 2025 % Result : Theorem 5.15s 5.41s % Output : Proof 5.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : ITP105^1 : TPTP v9.2.0. Released v7.5.0. % 0.11/0.13 % Command : duper %s % 0.13/0.33 % Computer : n010.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Thu Oct 2 22:21:53 EDT 2025 % 0.13/0.33 % CPUTime : % 5.15/5.41 SZS status Theorem for theBenchmark.p % 5.15/5.41 SZS output start Proof for theBenchmark.p % 5.15/5.41 Clause #1 (by assumption #[]): Eq (∀ (Xs : list_a), Eq (listSl97544552lice_a Xs zero_zero_nat) nil_list_a) True % 5.15/5.41 Clause #9 (by assumption #[]): Eq (∀ (Xs : list_a) (K : nat), ord_less_nat (size_size_list_a Xs) K → Eq (listSl97544552lice_a Xs K) nil_list_a) True % 5.15/5.41 Clause #57 (by assumption #[]): Eq (Eq (size_size_list_a nil_a) zero_zero_nat) True % 5.15/5.41 Clause #69 (by assumption #[]): Eq (∀ (N : nat), Ne N zero_zero_nat → ord_less_nat zero_zero_nat N) True % 5.15/5.41 Clause #327 (by assumption #[]): Eq (Not (Eq (listSl97544552lice_a nil_a k) nil_list_a)) True % 5.15/5.41 Clause #334 (by clausification #[1]): ∀ (a : list_a), Eq (Eq (listSl97544552lice_a a zero_zero_nat) nil_list_a) True % 5.15/5.41 Clause #335 (by clausification #[334]): ∀ (a : list_a), Eq (listSl97544552lice_a a zero_zero_nat) nil_list_a % 5.15/5.41 Clause #431 (by clausification #[69]): ∀ (a : nat), Eq (Ne a zero_zero_nat → ord_less_nat zero_zero_nat a) True % 5.15/5.41 Clause #432 (by clausification #[431]): ∀ (a : nat), Or (Eq (Ne a zero_zero_nat) False) (Eq (ord_less_nat zero_zero_nat a) True) % 5.15/5.41 Clause #433 (by clausification #[432]): ∀ (a : nat), Or (Eq (ord_less_nat zero_zero_nat a) True) (Eq a zero_zero_nat) % 5.15/5.41 Clause #459 (by clausification #[9]): ∀ (a : list_a), Eq (∀ (K : nat), ord_less_nat (size_size_list_a a) K → Eq (listSl97544552lice_a a K) nil_list_a) True % 5.15/5.41 Clause #460 (by clausification #[459]): ∀ (a : list_a) (a_1 : nat), Eq (ord_less_nat (size_size_list_a a) a_1 → Eq (listSl97544552lice_a a a_1) nil_list_a) True % 5.15/5.41 Clause #461 (by clausification #[460]): ∀ (a : list_a) (a_1 : nat), % 5.15/5.41 Or (Eq (ord_less_nat (size_size_list_a a) a_1) False) (Eq (Eq (listSl97544552lice_a a a_1) nil_list_a) True) % 5.15/5.41 Clause #462 (by clausification #[461]): ∀ (a : list_a) (a_1 : nat), % 5.15/5.41 Or (Eq (ord_less_nat (size_size_list_a a) a_1) False) (Eq (listSl97544552lice_a a a_1) nil_list_a) % 5.15/5.41 Clause #517 (by clausification #[57]): Eq (size_size_list_a nil_a) zero_zero_nat % 5.15/5.41 Clause #518 (by superposition #[517, 462]): ∀ (a : nat), Or (Eq (ord_less_nat zero_zero_nat a) False) (Eq (listSl97544552lice_a nil_a a) nil_list_a) % 5.15/5.41 Clause #957 (by superposition #[518, 433]): ∀ (a : nat), Or (Eq (listSl97544552lice_a nil_a a) nil_list_a) (Or (Eq False True) (Eq a zero_zero_nat)) % 5.15/5.41 Clause #978 (by clausification #[957]): ∀ (a : nat), Or (Eq (listSl97544552lice_a nil_a a) nil_list_a) (Eq a zero_zero_nat) % 5.15/5.41 Clause #980 (by superposition #[978, 335]): ∀ (a : nat) (a_1 : list_a), % 5.15/5.41 Or (Eq (listSl97544552lice_a nil_a a) nil_list_a) (Eq (listSl97544552lice_a a_1 a) nil_list_a) % 5.15/5.41 Clause #1119 (by equality factoring #[980]): ∀ (a : nat), Or (Ne nil_list_a nil_list_a) (Eq (listSl97544552lice_a nil_a a) nil_list_a) % 5.15/5.41 Clause #1148 (by eliminate resolved literals #[1119]): ∀ (a : nat), Eq (listSl97544552lice_a nil_a a) nil_list_a % 5.15/5.41 Clause #1439 (by clausification #[327]): Eq (Eq (listSl97544552lice_a nil_a k) nil_list_a) False % 5.15/5.41 Clause #1440 (by clausification #[1439]): Ne (listSl97544552lice_a nil_a k) nil_list_a % 5.15/5.41 Clause #1441 (by forward demodulation #[1440, 1148]): Ne nil_list_a nil_list_a % 5.15/5.41 Clause #1442 (by eliminate resolved literals #[1441]): False % 5.15/5.41 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------