%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP058^1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n005.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:08 PM UTC 2025 % Result : Theorem 23.94s 24.11s % Output : Proof 23.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : ITP058^1 : TPTP v9.2.0. Released v7.5.0. % 0.08/0.15 % Command : duper %s % 0.17/0.37 % Computer : n005.cluster.edu % 0.17/0.37 % Model : x86_64 x86_64 % 0.17/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.37 % Memory : 8042.1875MB % 0.17/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.37 % CPULimit : 300 % 0.17/0.37 % WCLimit : 300 % 0.17/0.37 % DateTime : Fri Oct 3 00:14:38 EDT 2025 % 0.17/0.37 % CPUTime : % 23.94/24.11 SZS status Theorem for theBenchmark.p % 23.94/24.11 SZS output start Proof for theBenchmark.p % 23.94/24.11 Clause #1 (by assumption #[]): Eq (Eq fe (fLPThe1519354920_p_v_s cfg fStepCfg fStepMsg)) True % 23.94/24.11 Clause #2 (by assumption #[]): Eq % 23.94/24.11 (∀ (Cfg : config256849571t_unit) (FStepCfg : list_c1059388851t_unit → list_message_p_v → list_c1059388851t_unit) % 23.94/24.11 (FStepMsg : list_c1059388851t_unit → list_message_p_v → list_message_p_v), % 23.94/24.11 Eq (fLPThe1519354920_p_v_s Cfg FStepCfg FStepMsg zero_zero_nat) (cons_c1162654829t_unit Cfg nil_co1338500125t_unit)) % 23.94/24.11 True % 23.94/24.11 Clause #318 (by assumption #[]): Eq (Not (Eq (fe zero_zero_nat) (cons_c1162654829t_unit cfg nil_co1338500125t_unit))) True % 23.94/24.11 Clause #341 (by clausification #[1]): Eq fe (fLPThe1519354920_p_v_s cfg fStepCfg fStepMsg) % 23.94/24.11 Clause #342 (by argument congruence #[341]): ∀ (a : nat), Eq (fe a) (fLPThe1519354920_p_v_s cfg fStepCfg fStepMsg a) % 23.94/24.11 Clause #349 (by clausification #[2]): ∀ (a : config256849571t_unit), % 23.94/24.11 Eq % 23.94/24.11 (∀ (FStepCfg : list_c1059388851t_unit → list_message_p_v → list_c1059388851t_unit) % 23.94/24.11 (FStepMsg : list_c1059388851t_unit → list_message_p_v → list_message_p_v), % 23.94/24.11 Eq (fLPThe1519354920_p_v_s a FStepCfg FStepMsg zero_zero_nat) (cons_c1162654829t_unit a nil_co1338500125t_unit)) % 23.94/24.11 True % 23.94/24.11 Clause #350 (by clausification #[349]): ∀ (a : config256849571t_unit) (a_1 : list_c1059388851t_unit → list_message_p_v → list_c1059388851t_unit), % 23.94/24.11 Eq % 23.94/24.11 (∀ (FStepMsg : list_c1059388851t_unit → list_message_p_v → list_message_p_v), % 23.94/24.11 Eq (fLPThe1519354920_p_v_s a a_1 FStepMsg zero_zero_nat) (cons_c1162654829t_unit a nil_co1338500125t_unit)) % 23.94/24.11 True % 23.94/24.11 Clause #351 (by clausification #[350]): ∀ (a : config256849571t_unit) (a_1 : list_c1059388851t_unit → list_message_p_v → list_c1059388851t_unit) % 23.94/24.11 (a_2 : list_c1059388851t_unit → list_message_p_v → list_message_p_v), % 23.94/24.11 Eq (Eq (fLPThe1519354920_p_v_s a a_1 a_2 zero_zero_nat) (cons_c1162654829t_unit a nil_co1338500125t_unit)) True % 23.94/24.11 Clause #352 (by clausification #[351]): ∀ (a : config256849571t_unit) (a_1 : list_c1059388851t_unit → list_message_p_v → list_c1059388851t_unit) % 23.94/24.11 (a_2 : list_c1059388851t_unit → list_message_p_v → list_message_p_v), % 23.94/24.11 Eq (fLPThe1519354920_p_v_s a a_1 a_2 zero_zero_nat) (cons_c1162654829t_unit a nil_co1338500125t_unit) % 23.94/24.11 Clause #917 (by superposition #[342, 352]): Eq (fe zero_zero_nat) (cons_c1162654829t_unit cfg nil_co1338500125t_unit) % 23.94/24.11 Clause #6917 (by clausification #[318]): Eq (Eq (fe zero_zero_nat) (cons_c1162654829t_unit cfg nil_co1338500125t_unit)) False % 23.94/24.11 Clause #6918 (by clausification #[6917]): Ne (fe zero_zero_nat) (cons_c1162654829t_unit cfg nil_co1338500125t_unit) % 23.94/24.11 Clause #6919 (by forward demodulation #[6918, 917]): Ne (fe zero_zero_nat) (fe zero_zero_nat) % 23.94/24.11 Clause #6920 (by eliminate resolved literals #[6919]): False % 23.94/24.11 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------