%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SCT179_5 : TPTP v9.2.0. Released v6.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:59:14 PM UTC 2025 % Result : Theorem 8.79s 8.99s % Output : Proof 8.79s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SCT179_5 : TPTP v9.2.0. Released v6.0.0. % 0.06/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 20:59:08 EDT 2025 % 0.14/0.35 % CPUTime : % 8.79/8.99 SZS status Theorem for theBenchmark.p % 8.79/8.99 SZS output start Proof for theBenchmark.p % 8.79/8.99 Clause #0 (by assumption #[]): Eq % 8.79/8.99 (∀ (A : Type) (R1 : fun (product_prod A A) bool) (A1 : fun A bool), % 8.79/8.99 order_1409979114der_on A A1 R1 → % 8.79/8.99 pp % 8.79/8.99 (aa (fun (product_prod A A) bool) bool (order_215145569der_on A A1) % 8.79/8.99 (minus_minus (fun (product_prod A A) bool) R1 (id A)))) % 8.79/8.99 True % 8.79/8.99 Clause #1 (by assumption #[]): Eq % 8.79/8.99 (Eq arrow_1985332922le_Lin % 8.79/8.99 (collect (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) % 8.79/8.99 (order_215145569der_on arrow_411405190le_alt (top_top (fun arrow_411405190le_alt bool))))) % 8.79/8.99 True % 8.79/8.99 Clause #11 (by assumption #[]): Eq (∀ (A : Type), Eq (top_top (fun A bool)) (collect A (combk bool A fTrue))) True % 8.79/8.99 Clause #74 (by assumption #[]): Eq (∀ (A : Type) (P1 : fun A bool), Eq (collect A P1) P1) True % 8.79/8.99 Clause #115 (by assumption #[]): Eq (order_1409979114der_on arrow_411405190le_alt (top_top (fun arrow_411405190le_alt bool)) r) True % 8.79/8.99 Clause #117 (by assumption #[]): Eq % 8.79/8.99 (Not % 8.79/8.99 (Exists fun L => % 8.79/8.99 pp % 8.79/8.99 (aa (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) bool % 8.79/8.99 (order_215145569der_on arrow_411405190le_alt (top_top (fun arrow_411405190le_alt bool))) L))) % 8.79/8.99 True % 8.79/8.99 Clause #118 (by clausification #[0]): ∀ (a : Type), % 8.79/8.99 Eq % 8.79/8.99 (∀ (R1 : fun (product_prod a a) bool) (A1 : fun a bool), % 8.79/8.99 order_1409979114der_on a A1 R1 → % 8.79/8.99 pp % 8.79/8.99 (aa (fun (product_prod a a) bool) bool (order_215145569der_on a A1) % 8.79/8.99 (minus_minus (fun (product_prod a a) bool) R1 (id a)))) % 8.79/8.99 True % 8.79/8.99 Clause #119 (by clausification #[118]): ∀ (a : Type) (a_1 : fun (product_prod a a) bool), % 8.79/8.99 Eq % 8.79/8.99 (∀ (A1 : fun a bool), % 8.79/8.99 order_1409979114der_on a A1 a_1 → % 8.79/8.99 pp % 8.79/8.99 (aa (fun (product_prod a a) bool) bool (order_215145569der_on a A1) % 8.79/8.99 (minus_minus (fun (product_prod a a) bool) a_1 (id a)))) % 8.79/8.99 True % 8.79/8.99 Clause #120 (by clausification #[119]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : fun (product_prod a a) bool), % 8.79/8.99 Eq % 8.79/8.99 (order_1409979114der_on a a_1 a_2 → % 8.79/8.99 pp % 8.79/8.99 (aa (fun (product_prod a a) bool) bool (order_215145569der_on a a_1) % 8.79/8.99 (minus_minus (fun (product_prod a a) bool) a_2 (id a)))) % 8.79/8.99 True % 8.79/8.99 Clause #121 (by clausification #[120]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : fun (product_prod a a) bool), % 8.79/8.99 Or (Eq (order_1409979114der_on a a_1 a_2) False) % 8.79/8.99 (Eq % 8.79/8.99 (pp % 8.79/8.99 (aa (fun (product_prod a a) bool) bool (order_215145569der_on a a_1) % 8.79/8.99 (minus_minus (fun (product_prod a a) bool) a_2 (id a)))) % 8.79/8.99 True) % 8.79/8.99 Clause #127 (by superposition #[115, 121]): Or % 8.79/8.99 (Eq % 8.79/8.99 (pp % 8.79/8.99 (aa (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) bool % 8.79/8.99 (order_215145569der_on arrow_411405190le_alt (top_top (fun arrow_411405190le_alt bool))) % 8.79/8.99 (minus_minus (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) r % 8.79/8.99 (id arrow_411405190le_alt)))) % 8.79/8.99 True) % 8.79/8.99 (Eq False True) % 8.79/8.99 Clause #128 (by clausification #[1]): Eq arrow_1985332922le_Lin % 8.79/8.99 (collect (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) % 8.79/8.99 (order_215145569der_on arrow_411405190le_alt (top_top (fun arrow_411405190le_alt bool)))) % 8.79/8.99 Clause #362 (by clausification #[11]): ∀ (a : Type), Eq (Eq (top_top (fun a bool)) (collect a (combk bool a fTrue))) True % 8.79/8.99 Clause #363 (by clausification #[362]): ∀ (a : Type), Eq (top_top (fun a bool)) (collect a (combk bool a fTrue)) % 8.79/8.99 Clause #2555 (by clausification #[74]): ∀ (a : Type), Eq (∀ (P1 : fun a bool), Eq (collect a P1) P1) True % 8.79/8.99 Clause #2556 (by clausification #[2555]): ∀ (a : Type) (a_1 : fun a bool), Eq (Eq (collect a a_1) a_1) True % 8.79/8.99 Clause #2557 (by clausification #[2556]): ∀ (a : Type) (a_1 : fun a bool), Eq (collect a a_1) a_1 % 8.79/8.99 Clause #2560 (by superposition #[2557, 128]): Eq arrow_1985332922le_Lin (order_215145569der_on arrow_411405190le_alt (top_top (fun arrow_411405190le_alt bool))) % 8.79/8.99 Clause #2561 (by superposition #[2557, 363]): ∀ (a : Type), Eq (top_top (fun a bool)) (combk bool a fTrue) % 8.79/8.99 Clause #2621 (by backward demodulation #[2561, 2560]): Eq arrow_1985332922le_Lin (order_215145569der_on arrow_411405190le_alt (combk bool arrow_411405190le_alt fTrue)) % 8.79/9.02 Clause #4448 (by clausification #[117]): Eq % 8.79/9.02 (Exists fun L => % 8.79/9.02 pp % 8.79/9.02 (aa (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) bool % 8.79/9.02 (order_215145569der_on arrow_411405190le_alt (top_top (fun arrow_411405190le_alt bool))) L)) % 8.79/9.02 False % 8.79/9.02 Clause #4449 (by clausification #[4448]): ∀ (a : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 8.79/9.02 Eq % 8.79/9.02 (pp % 8.79/9.02 (aa (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) bool % 8.79/9.02 (order_215145569der_on arrow_411405190le_alt (top_top (fun arrow_411405190le_alt bool))) a)) % 8.79/9.02 False % 8.79/9.02 Clause #4450 (by forward demodulation #[4449, 2561]): ∀ (a : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 8.79/9.02 Eq % 8.79/9.02 (pp % 8.79/9.02 (aa (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) bool % 8.79/9.02 (order_215145569der_on arrow_411405190le_alt (combk bool arrow_411405190le_alt fTrue)) a)) % 8.79/9.02 False % 8.79/9.02 Clause #4451 (by forward demodulation #[4450, 2621]): ∀ (a : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 8.79/9.02 Eq (pp (aa (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) bool arrow_1985332922le_Lin a)) False % 8.79/9.02 Clause #4516 (by clausification #[127]): Eq % 8.79/9.02 (pp % 8.79/9.02 (aa (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) bool % 8.79/9.02 (order_215145569der_on arrow_411405190le_alt (top_top (fun arrow_411405190le_alt bool))) % 8.79/9.02 (minus_minus (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) r (id arrow_411405190le_alt)))) % 8.79/9.02 True % 8.79/9.02 Clause #4517 (by forward demodulation #[4516, 2561]): Eq % 8.79/9.02 (pp % 8.79/9.02 (aa (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) bool % 8.79/9.02 (order_215145569der_on arrow_411405190le_alt (combk bool arrow_411405190le_alt fTrue)) % 8.79/9.02 (minus_minus (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) r (id arrow_411405190le_alt)))) % 8.79/9.02 True % 8.79/9.02 Clause #4518 (by forward demodulation #[4517, 2621]): Eq % 8.79/9.02 (pp % 8.79/9.02 (aa (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) bool arrow_1985332922le_Lin % 8.79/9.02 (minus_minus (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) r (id arrow_411405190le_alt)))) % 8.79/9.02 True % 8.79/9.02 Clause #4521 (by superposition #[4518, 4451]): Eq True False % 8.79/9.02 Clause #4581 (by clausification #[4521]): False % 8.79/9.02 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------