%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP224_1 : TPTP v9.2.0. Released v8.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n001.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:34 PM UTC 2025 % Result : Theorem 116.94s 117.13s % Output : Proof 116.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ITP224_1 : TPTP v9.2.0. Released v8.0.0. % 0.13/0.14 % Command : duper %s % 0.13/0.35 % Computer : n001.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 00:27:08 EDT 2025 % 0.13/0.35 % CPUTime : % 116.94/117.13 SZS status Theorem for theBenchmark.p % 116.94/117.13 SZS output start Proof for theBenchmark.p % 116.94/117.13 Clause #0 (by assumption #[]): Eq (Not (pp (aa_nat_bool (vEBT_invar_vebt summary) zero_zero_nat))) True % 116.94/117.13 Clause #211 (by assumption #[]): Eq % 116.94/117.13 (∀ (A B : nat), % 116.94/117.13 Iff (pp (aa_nat_bool (aa_nat_fun_nat_bool ord_less_eq_nat A) B)) % 116.94/117.13 (Exists fun C2 => Eq B (aa_nat_nat (aa_nat_fun_nat_nat plus_plus_nat A) C2))) % 116.94/117.13 True % 116.94/117.13 Clause #389 (by assumption #[]): Eq (∀ (A : nat), pp (aa_nat_bool (aa_nat_fun_nat_bool ord_less_eq_nat A) zero_zero_nat) → Eq A zero_zero_nat) True % 116.94/117.13 Clause #10489 (by assumption #[]): Eq (Eq zero_zero_nat deg) True % 116.94/117.13 Clause #10491 (by assumption #[]): Eq (pp (aa_nat_bool (vEBT_invar_vebt summary) m)) True % 116.94/117.13 Clause #10493 (by assumption #[]): Eq (Eq m na) True % 116.94/117.13 Clause #10494 (by assumption #[]): Eq (Eq deg (aa_nat_nat (aa_nat_fun_nat_nat plus_plus_nat na) m)) True % 116.94/117.13 Clause #10498 (by clausification #[0]): Eq (pp (aa_nat_bool (vEBT_invar_vebt summary) zero_zero_nat)) False % 116.94/117.13 Clause #10507 (by clausification #[10493]): Eq m na % 116.94/117.13 Clause #10508 (by clausification #[10489]): Eq zero_zero_nat deg % 116.94/117.13 Clause #10971 (by clausification #[389]): ∀ (a : nat), Eq (pp (aa_nat_bool (aa_nat_fun_nat_bool ord_less_eq_nat a) zero_zero_nat) → Eq a zero_zero_nat) True % 116.94/117.13 Clause #10972 (by clausification #[10971]): ∀ (a : nat), % 116.94/117.13 Or (Eq (pp (aa_nat_bool (aa_nat_fun_nat_bool ord_less_eq_nat a) zero_zero_nat)) False) (Eq (Eq a zero_zero_nat) True) % 116.94/117.13 Clause #10973 (by clausification #[10972]): ∀ (a : nat), Or (Eq (pp (aa_nat_bool (aa_nat_fun_nat_bool ord_less_eq_nat a) zero_zero_nat)) False) (Eq a zero_zero_nat) % 116.94/117.13 Clause #15037 (by clausification #[211]): ∀ (a : nat), % 116.94/117.13 Eq % 116.94/117.13 (∀ (B : nat), % 116.94/117.13 Iff (pp (aa_nat_bool (aa_nat_fun_nat_bool ord_less_eq_nat a) B)) % 116.94/117.13 (Exists fun C2 => Eq B (aa_nat_nat (aa_nat_fun_nat_nat plus_plus_nat a) C2))) % 116.94/117.13 True % 116.94/117.13 Clause #15038 (by clausification #[15037]): ∀ (a a_1 : nat), % 116.94/117.13 Eq % 116.94/117.13 (Iff (pp (aa_nat_bool (aa_nat_fun_nat_bool ord_less_eq_nat a) a_1)) % 116.94/117.13 (Exists fun C2 => Eq a_1 (aa_nat_nat (aa_nat_fun_nat_nat plus_plus_nat a) C2))) % 116.94/117.13 True % 116.94/117.13 Clause #15039 (by clausification #[15038]): ∀ (a a_1 : nat), % 116.94/117.13 Or (Eq (pp (aa_nat_bool (aa_nat_fun_nat_bool ord_less_eq_nat a) a_1)) True) % 116.94/117.13 (Eq (Exists fun C2 => Eq a_1 (aa_nat_nat (aa_nat_fun_nat_nat plus_plus_nat a) C2)) False) % 116.94/117.13 Clause #15041 (by clausification #[15039]): ∀ (a a_1 a_2 : nat), % 116.94/117.13 Or (Eq (pp (aa_nat_bool (aa_nat_fun_nat_bool ord_less_eq_nat a) a_1)) True) % 116.94/117.13 (Eq (Eq a_1 (aa_nat_nat (aa_nat_fun_nat_nat plus_plus_nat a) a_2)) False) % 116.94/117.13 Clause #15042 (by clausification #[15041]): ∀ (a a_1 a_2 : nat), % 116.94/117.13 Or (Eq (pp (aa_nat_bool (aa_nat_fun_nat_bool ord_less_eq_nat a) a_1)) True) % 116.94/117.13 (Ne a_1 (aa_nat_nat (aa_nat_fun_nat_nat plus_plus_nat a) a_2)) % 116.94/117.13 Clause #15043 (by destructive equality resolution #[15042]): ∀ (a a_1 : nat), % 116.94/117.13 Eq (pp (aa_nat_bool (aa_nat_fun_nat_bool ord_less_eq_nat a) (aa_nat_nat (aa_nat_fun_nat_nat plus_plus_nat a) a_1))) % 116.94/117.13 True % 116.94/117.13 Clause #15626 (by clausification #[10494]): Eq deg (aa_nat_nat (aa_nat_fun_nat_nat plus_plus_nat na) m) % 116.94/117.13 Clause #15627 (by forward demodulation #[15626, 10508]): Eq zero_zero_nat (aa_nat_nat (aa_nat_fun_nat_nat plus_plus_nat na) m) % 116.94/117.13 Clause #15628 (by forward demodulation #[15627, 10507]): Eq zero_zero_nat (aa_nat_nat (aa_nat_fun_nat_nat plus_plus_nat m) m) % 116.94/117.13 Clause #15641 (by superposition #[15628, 15043]): Eq (pp (aa_nat_bool (aa_nat_fun_nat_bool ord_less_eq_nat m) zero_zero_nat)) True % 116.94/117.13 Clause #15651 (by superposition #[15641, 10973]): Or (Eq True False) (Eq m zero_zero_nat) % 116.94/117.13 Clause #15670 (by clausification #[15651]): Eq m zero_zero_nat % 116.94/117.13 Clause #15672 (by backward demodulation #[15670, 10491]): Eq (pp (aa_nat_bool (vEBT_invar_vebt summary) zero_zero_nat)) True % 116.94/117.13 Clause #15676 (by superposition #[15672, 10498]): Eq True False % 116.94/117.13 Clause #15691 (by clausification #[15676]): False % 116.94/117.13 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------