%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP056^1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n027.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:07 PM UTC 2025 % Result : Theorem 40.77s 40.98s % Output : Proof 40.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : ITP056^1 : TPTP v9.2.0. Released v7.5.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n027.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 22:57:38 EDT 2025 % 0.13/0.35 % CPUTime : % 40.77/40.98 SZS status Theorem for theBenchmark.p % 40.77/40.98 SZS output start Proof for theBenchmark.p % 40.77/40.98 Clause #0 (by assumption #[]): Eq (Ne (fe n) nil_co1338500125t_unit) True % 40.77/40.98 Clause #1 (by assumption #[]): Eq % 40.77/40.98 (∀ (L : list_c1059388851t_unit), % 40.77/40.98 Ne L nil_co1338500125t_unit → % 40.77/40.98 Eq (last_c571238084t_unit L) (nth_co1649820636t_unit L (minus_minus_nat (size_s1406904903t_unit L) one_one_nat))) % 40.77/40.98 True % 40.77/40.98 Clause #165 (by assumption #[]): Eq % 40.77/40.98 (Not % 40.77/40.98 (Eq (last_c571238084t_unit (fe n)) % 40.77/40.98 (nth_co1649820636t_unit (fe n) (minus_minus_nat (size_s1406904903t_unit (fe n)) one_one_nat)))) % 40.77/40.98 True % 40.77/40.98 Clause #179 (by clausification #[0]): Ne (fe n) nil_co1338500125t_unit % 40.77/40.98 Clause #221 (by clausification #[1]): ∀ (a : list_c1059388851t_unit), % 40.77/40.98 Eq % 40.77/40.98 (Ne a nil_co1338500125t_unit → % 40.77/40.98 Eq (last_c571238084t_unit a) (nth_co1649820636t_unit a (minus_minus_nat (size_s1406904903t_unit a) one_one_nat))) % 40.77/40.98 True % 40.77/40.98 Clause #222 (by clausification #[221]): ∀ (a : list_c1059388851t_unit), % 40.77/40.98 Or (Eq (Ne a nil_co1338500125t_unit) False) % 40.77/40.98 (Eq % 40.77/40.98 (Eq (last_c571238084t_unit a) (nth_co1649820636t_unit a (minus_minus_nat (size_s1406904903t_unit a) one_one_nat))) % 40.77/40.98 True) % 40.77/40.98 Clause #223 (by clausification #[222]): ∀ (a : list_c1059388851t_unit), % 40.77/40.98 Or % 40.77/40.98 (Eq % 40.77/40.98 (Eq (last_c571238084t_unit a) (nth_co1649820636t_unit a (minus_minus_nat (size_s1406904903t_unit a) one_one_nat))) % 40.77/40.98 True) % 40.77/40.98 (Eq a nil_co1338500125t_unit) % 40.77/40.98 Clause #224 (by clausification #[223]): ∀ (a : list_c1059388851t_unit), % 40.77/40.98 Or (Eq a nil_co1338500125t_unit) % 40.77/40.98 (Eq (last_c571238084t_unit a) (nth_co1649820636t_unit a (minus_minus_nat (size_s1406904903t_unit a) one_one_nat))) % 40.77/40.98 Clause #14028 (by clausification #[165]): Eq % 40.77/40.98 (Eq (last_c571238084t_unit (fe n)) % 40.77/40.98 (nth_co1649820636t_unit (fe n) (minus_minus_nat (size_s1406904903t_unit (fe n)) one_one_nat))) % 40.77/40.98 False % 40.77/40.98 Clause #14029 (by clausification #[14028]): Ne (last_c571238084t_unit (fe n)) % 40.77/40.98 (nth_co1649820636t_unit (fe n) (minus_minus_nat (size_s1406904903t_unit (fe n)) one_one_nat)) % 40.77/40.98 Clause #14030 (by superposition #[14029, 224]): Or (Eq (fe n) nil_co1338500125t_unit) (Ne (last_c571238084t_unit (fe n)) (last_c571238084t_unit (fe n))) % 40.77/40.98 Clause #14039 (by eliminate resolved literals #[14030]): Eq (fe n) nil_co1338500125t_unit % 40.77/40.98 Clause #14040 (by forward contextual literal cutting #[14039, 179]): False % 40.77/40.98 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------