%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP151^1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.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:19 PM UTC 2025 % Result : Theorem 5.86s 6.09s % Output : Proof 5.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP151^1 : TPTP v9.2.0. Released v7.5.0. % 0.12/0.13 % Command : duper %s % 0.12/0.34 % Computer : n014.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Oct 2 22:20:23 EDT 2025 % 0.12/0.34 % CPUTime : % 5.86/6.09 SZS status Theorem for theBenchmark.p % 5.86/6.09 SZS output start Proof for theBenchmark.p % 5.86/6.09 Clause #1 (by assumption #[]): Eq (∀ (N : nat), Not (ord_less_nat N zero_zero_nat)) True % 5.86/6.09 Clause #22 (by assumption #[]): Eq % 5.86/6.09 (∀ (P3 : polyno727731844poly_a) (N : nat), % 5.86/6.09 polyno1372495879olyh_a P3 (suc N) → Eq (polyno578545843gree_a P3) zero_zero_nat) % 5.86/6.09 True % 5.86/6.09 Clause #45 (by assumption #[]): Eq (∀ (X : nat), Ne X zero_zero_nat → Not (∀ (V : nat), Ne X (suc V))) True % 5.86/6.09 Clause #286 (by assumption #[]): Eq (ord_less_nat zero_zero_nat n) True % 5.86/6.09 Clause #287 (by assumption #[]): Eq (polyno1372495879olyh_a p n) True % 5.86/6.09 Clause #288 (by assumption #[]): Eq (Not (Eq (polyno578545843gree_a p) zero_zero_nat)) True % 5.86/6.09 Clause #300 (by clausification #[1]): ∀ (a : nat), Eq (Not (ord_less_nat a zero_zero_nat)) True % 5.86/6.09 Clause #301 (by clausification #[300]): ∀ (a : nat), Eq (ord_less_nat a zero_zero_nat) False % 5.86/6.09 Clause #656 (by clausification #[288]): Eq (Eq (polyno578545843gree_a p) zero_zero_nat) False % 5.86/6.09 Clause #657 (by clausification #[656]): Ne (polyno578545843gree_a p) zero_zero_nat % 5.86/6.09 Clause #1079 (by clausification #[22]): ∀ (a : polyno727731844poly_a), % 5.86/6.09 Eq (∀ (N : nat), polyno1372495879olyh_a a (suc N) → Eq (polyno578545843gree_a a) zero_zero_nat) True % 5.86/6.09 Clause #1080 (by clausification #[1079]): ∀ (a : polyno727731844poly_a) (a_1 : nat), % 5.86/6.09 Eq (polyno1372495879olyh_a a (suc a_1) → Eq (polyno578545843gree_a a) zero_zero_nat) True % 5.86/6.09 Clause #1081 (by clausification #[1080]): ∀ (a : polyno727731844poly_a) (a_1 : nat), % 5.86/6.09 Or (Eq (polyno1372495879olyh_a a (suc a_1)) False) (Eq (Eq (polyno578545843gree_a a) zero_zero_nat) True) % 5.86/6.09 Clause #1082 (by clausification #[1081]): ∀ (a : polyno727731844poly_a) (a_1 : nat), % 5.86/6.09 Or (Eq (polyno1372495879olyh_a a (suc a_1)) False) (Eq (polyno578545843gree_a a) zero_zero_nat) % 5.86/6.09 Clause #1816 (by clausification #[45]): ∀ (a : nat), Eq (Ne a zero_zero_nat → Not (∀ (V : nat), Ne a (suc V))) True % 5.86/6.09 Clause #1817 (by clausification #[1816]): ∀ (a : nat), Or (Eq (Ne a zero_zero_nat) False) (Eq (Not (∀ (V : nat), Ne a (suc V))) True) % 5.86/6.09 Clause #1818 (by clausification #[1817]): ∀ (a : nat), Or (Eq (Not (∀ (V : nat), Ne a (suc V))) True) (Eq a zero_zero_nat) % 5.86/6.09 Clause #1819 (by clausification #[1818]): ∀ (a : nat), Or (Eq a zero_zero_nat) (Eq (∀ (V : nat), Ne a (suc V)) False) % 5.86/6.09 Clause #1820 (by clausification #[1819]): ∀ (a a_1 : nat), Or (Eq a zero_zero_nat) (Eq (Not (Ne a (suc (skS.0 8 a a_1)))) True) % 5.86/6.09 Clause #1821 (by clausification #[1820]): ∀ (a a_1 : nat), Or (Eq a zero_zero_nat) (Eq (Ne a (suc (skS.0 8 a a_1))) False) % 5.86/6.09 Clause #1822 (by clausification #[1821]): ∀ (a a_1 : nat), Or (Eq a zero_zero_nat) (Eq a (suc (skS.0 8 a a_1))) % 5.86/6.09 Clause #1859 (by superposition #[1822, 1082]): ∀ (a : nat) (a_1 : polyno727731844poly_a), % 5.86/6.09 Or (Eq a zero_zero_nat) (Or (Eq (polyno1372495879olyh_a a_1 a) False) (Eq (polyno578545843gree_a a_1) zero_zero_nat)) % 5.86/6.09 Clause #2070 (by superposition #[1859, 287]): Or (Eq n zero_zero_nat) (Or (Eq (polyno578545843gree_a p) zero_zero_nat) (Eq False True)) % 5.86/6.09 Clause #2080 (by clausification #[2070]): Or (Eq n zero_zero_nat) (Eq (polyno578545843gree_a p) zero_zero_nat) % 5.86/6.09 Clause #2081 (by forward contextual literal cutting #[2080, 657]): Eq n zero_zero_nat % 5.86/6.09 Clause #2083 (by backward demodulation #[2081, 286]): Eq (ord_less_nat zero_zero_nat zero_zero_nat) True % 5.86/6.09 Clause #2097 (by superposition #[2083, 301]): Eq True False % 5.86/6.09 Clause #2118 (by clausification #[2097]): False % 5.86/6.09 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------