%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : DAT162^1 : TPTP v9.2.0. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n011.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:47:14 PM UTC 2025 % Result : Theorem 64.47s 64.64s % Output : Proof 64.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : DAT162^1 : TPTP v9.2.0. Released v7.0.0. % 0.13/0.13 % Command : duper %s % 0.14/0.34 % Computer : n011.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu Oct 2 21:39:08 EDT 2025 % 0.14/0.34 % CPUTime : % 64.47/64.64 SZS status Theorem for theBenchmark.p % 64.47/64.64 SZS output start Proof for theBenchmark.p % 64.47/64.64 Clause #0 (by assumption #[]): Eq (hammin1195055315smooth n2) True % 64.47/64.64 Clause #1 (by assumption #[]): Eq (ord_less nat n2 na) True % 64.47/64.64 Clause #2 (by assumption #[]): Eq % 64.47/64.64 (∀ (Y : nat), % 64.47/64.64 ord_less nat Y na → hammin1195055315smooth Y → member nat Y (coinductive_lset nat hammin2015774020amming)) % 64.47/64.64 True % 64.47/64.64 Clause #261 (by assumption #[]): Eq (Not (member nat n2 (coinductive_lset nat hammin2015774020amming))) True % 64.47/64.64 Clause #262 (by clausification #[2]): ∀ (a : nat), % 64.47/64.64 Eq (ord_less nat a na → hammin1195055315smooth a → member nat a (coinductive_lset nat hammin2015774020amming)) True % 64.47/64.64 Clause #263 (by clausification #[262]): ∀ (a : nat), % 64.47/64.64 Or (Eq (ord_less nat a na) False) % 64.47/64.64 (Eq (hammin1195055315smooth a → member nat a (coinductive_lset nat hammin2015774020amming)) True) % 64.47/64.64 Clause #264 (by clausification #[263]): ∀ (a : nat), % 64.47/64.64 Or (Eq (ord_less nat a na) False) % 64.47/64.64 (Or (Eq (hammin1195055315smooth a) False) (Eq (member nat a (coinductive_lset nat hammin2015774020amming)) True)) % 64.47/64.64 Clause #265 (by superposition #[264, 1]): Or (Eq (hammin1195055315smooth n2) False) % 64.47/64.64 (Or (Eq (member nat n2 (coinductive_lset nat hammin2015774020amming)) True) (Eq False True)) % 64.47/64.64 Clause #479 (by clausification #[261]): Eq (member nat n2 (coinductive_lset nat hammin2015774020amming)) False % 64.47/64.64 Clause #17235 (by clausification #[265]): Or (Eq (hammin1195055315smooth n2) False) (Eq (member nat n2 (coinductive_lset nat hammin2015774020amming)) True) % 64.47/64.64 Clause #17236 (by forward demodulation #[17235, 0]): Or (Eq True False) (Eq (member nat n2 (coinductive_lset nat hammin2015774020amming)) True) % 64.47/64.64 Clause #17237 (by clausification #[17236]): Eq (member nat n2 (coinductive_lset nat hammin2015774020amming)) True % 64.47/64.64 Clause #17238 (by superposition #[17237, 479]): Eq True False % 64.47/64.64 Clause #17298 (by clausification #[17238]): False % 64.47/64.64 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------