%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SCT240_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n010.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:17 PM UTC 2025 % Result : Theorem 64.49s 64.68s % Output : Proof 64.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SCT240_5 : TPTP v9.2.0. Released v6.0.0. % 0.15/0.14 % Command : duper %s % 0.15/0.35 % Computer : n010.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Thu Oct 2 21:20:38 EDT 2025 % 0.15/0.36 % CPUTime : % 64.49/64.68 SZS status Theorem for theBenchmark.p % 64.49/64.68 SZS output start Proof for theBenchmark.p % 64.49/64.68 Clause #0 (by assumption #[]): Eq (Ne a b) True % 64.49/64.68 Clause #3 (by assumption #[]): Eq % 64.49/64.68 (∀ (Ba Aa : arrow_411405190le_alt), % 64.49/64.68 Ne Aa Ba → % 64.49/64.68 Exists fun X1 => % 64.49/64.68 And (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) X1 arrow_1985332922le_Lin) % 64.49/64.68 (member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.68 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.68 (aa arrow_411405190le_alt % 64.49/64.68 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.68 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) Aa) % 64.49/64.68 Ba) % 64.49/64.68 X1)) % 64.49/64.68 True % 64.49/64.68 Clause #112 (by assumption #[]): Eq % 64.49/64.68 (∀ (Lab : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.68 member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.68 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.68 (aa arrow_411405190le_alt % 64.49/64.68 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.68 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) a) % 64.49/64.68 b) % 64.49/64.68 Lab → % 64.49/64.68 member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) Lab arrow_1985332922le_Lin → thesis) % 64.49/64.68 True % 64.49/64.68 Clause #113 (by assumption #[]): Eq (Not thesis) True % 64.49/64.68 Clause #114 (by clausification #[113]): Eq thesis False % 64.49/64.68 Clause #116 (by clausification #[0]): Ne a b % 64.49/64.68 Clause #117 (by clausification #[112]): ∀ (a_1 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.68 Eq % 64.49/64.68 (member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.68 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.68 (aa arrow_411405190le_alt % 64.49/64.68 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.68 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) a) % 64.49/64.68 b) % 64.49/64.68 a_1 → % 64.49/64.68 member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) a_1 arrow_1985332922le_Lin → thesis) % 64.49/64.68 True % 64.49/64.68 Clause #118 (by clausification #[117]): ∀ (a_1 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.68 Or % 64.49/64.68 (Eq % 64.49/64.68 (member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.68 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.68 (aa arrow_411405190le_alt % 64.49/64.68 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.68 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) a) % 64.49/64.68 b) % 64.49/64.68 a_1) % 64.49/64.68 False) % 64.49/64.68 (Eq % 64.49/64.68 (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) a_1 arrow_1985332922le_Lin → thesis) % 64.49/64.68 True) % 64.49/64.68 Clause #119 (by clausification #[118]): ∀ (a_1 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.68 Or % 64.49/64.68 (Eq % 64.49/64.68 (member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.68 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.68 (aa arrow_411405190le_alt % 64.49/64.68 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.68 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) a) % 64.49/64.68 b) % 64.49/64.68 a_1) % 64.49/64.68 False) % 64.49/64.68 (Or % 64.49/64.68 (Eq (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) a_1 arrow_1985332922le_Lin) % 64.49/64.68 False) % 64.49/64.68 (Eq thesis True)) % 64.49/64.68 Clause #120 (by forward demodulation #[119, 114]): ∀ (a_1 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.68 Or % 64.49/64.68 (Eq % 64.49/64.68 (member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.68 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.68 (aa arrow_411405190le_alt % 64.49/64.68 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.69 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) a) % 64.49/64.69 b) % 64.49/64.69 a_1) % 64.49/64.69 False) % 64.49/64.69 (Or % 64.49/64.69 (Eq (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) a_1 arrow_1985332922le_Lin) % 64.49/64.69 False) % 64.49/64.69 (Eq False True)) % 64.49/64.69 Clause #121 (by clausification #[120]): ∀ (a_1 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.69 Or % 64.49/64.69 (Eq % 64.49/64.69 (member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.69 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.69 (aa arrow_411405190le_alt % 64.49/64.69 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.69 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) a) % 64.49/64.69 b) % 64.49/64.69 a_1) % 64.49/64.69 False) % 64.49/64.69 (Eq (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) a_1 arrow_1985332922le_Lin) False) % 64.49/64.69 Clause #223 (by clausification #[3]): ∀ (a : arrow_411405190le_alt), % 64.49/64.69 Eq % 64.49/64.69 (∀ (Aa : arrow_411405190le_alt), % 64.49/64.69 Ne Aa a → % 64.49/64.69 Exists fun X1 => % 64.49/64.69 And (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) X1 arrow_1985332922le_Lin) % 64.49/64.69 (member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.69 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.69 (aa arrow_411405190le_alt % 64.49/64.69 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.69 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) Aa) % 64.49/64.69 a) % 64.49/64.69 X1)) % 64.49/64.69 True % 64.49/64.69 Clause #224 (by clausification #[223]): ∀ (a a_1 : arrow_411405190le_alt), % 64.49/64.69 Eq % 64.49/64.69 (Ne a a_1 → % 64.49/64.69 Exists fun X1 => % 64.49/64.69 And (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) X1 arrow_1985332922le_Lin) % 64.49/64.69 (member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.69 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.69 (aa arrow_411405190le_alt % 64.49/64.69 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.69 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) a) % 64.49/64.69 a_1) % 64.49/64.69 X1)) % 64.49/64.69 True % 64.49/64.69 Clause #225 (by clausification #[224]): ∀ (a a_1 : arrow_411405190le_alt), % 64.49/64.69 Or (Eq (Ne a a_1) False) % 64.49/64.69 (Eq % 64.49/64.69 (Exists fun X1 => % 64.49/64.69 And (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) X1 arrow_1985332922le_Lin) % 64.49/64.69 (member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.69 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.69 (aa arrow_411405190le_alt % 64.49/64.69 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.69 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) a) % 64.49/64.69 a_1) % 64.49/64.69 X1)) % 64.49/64.69 True) % 64.49/64.69 Clause #226 (by clausification #[225]): ∀ (a a_1 : arrow_411405190le_alt), % 64.49/64.69 Or % 64.49/64.69 (Eq % 64.49/64.69 (Exists fun X1 => % 64.49/64.69 And (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) X1 arrow_1985332922le_Lin) % 64.49/64.69 (member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.69 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.69 (aa arrow_411405190le_alt % 64.49/64.69 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.69 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) a) % 64.49/64.69 a_1) % 64.49/64.69 X1)) % 64.49/64.69 True) % 64.49/64.69 (Eq a a_1) % 64.49/64.69 Clause #227 (by clausification #[226]): ∀ (a a_1 : arrow_411405190le_alt) (a_2 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.69 Or (Eq a a_1) % 64.49/64.69 (Eq % 64.49/64.69 (And % 64.49/64.69 (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) (skS.0 4 a a_1 a_2) % 64.49/64.69 arrow_1985332922le_Lin) % 64.49/64.69 (member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.74 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.74 (aa arrow_411405190le_alt % 64.49/64.74 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.74 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) a) % 64.49/64.74 a_1) % 64.49/64.74 (skS.0 4 a a_1 a_2))) % 64.49/64.74 True) % 64.49/64.74 Clause #228 (by clausification #[227]): ∀ (a a_1 : arrow_411405190le_alt) (a_2 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.74 Or (Eq a a_1) % 64.49/64.74 (Eq % 64.49/64.74 (member (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.74 (aa arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt) % 64.49/64.74 (aa arrow_411405190le_alt % 64.49/64.74 (fun arrow_411405190le_alt (product_prod arrow_411405190le_alt arrow_411405190le_alt)) % 64.49/64.74 (product_Pair arrow_411405190le_alt arrow_411405190le_alt) a) % 64.49/64.74 a_1) % 64.49/64.74 (skS.0 4 a a_1 a_2)) % 64.49/64.74 True) % 64.49/64.74 Clause #229 (by clausification #[227]): ∀ (a a_1 : arrow_411405190le_alt) (a_2 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.74 Or (Eq a a_1) % 64.49/64.74 (Eq % 64.49/64.74 (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) (skS.0 4 a a_1 a_2) % 64.49/64.74 arrow_1985332922le_Lin) % 64.49/64.74 True) % 64.49/64.74 Clause #244 (by superposition #[228, 121]): ∀ (a_1 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.74 Or (Eq a b) % 64.49/64.74 (Or (Eq True False) % 64.49/64.74 (Eq % 64.49/64.74 (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) (skS.0 4 a b a_1) % 64.49/64.74 arrow_1985332922le_Lin) % 64.49/64.74 False)) % 64.49/64.74 Clause #1991 (by superposition #[229, 116]): ∀ (a_1 : arrow_411405190le_alt) (a_2 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.74 Or % 64.49/64.74 (Eq % 64.49/64.74 (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) (skS.0 4 a a_1 a_2) % 64.49/64.74 arrow_1985332922le_Lin) % 64.49/64.74 True) % 64.49/64.74 (Ne a_1 b) % 64.49/64.74 Clause #2124 (by destructive equality resolution #[1991]): ∀ (a_1 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.74 Eq % 64.49/64.74 (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) (skS.0 4 a b a_1) % 64.49/64.74 arrow_1985332922le_Lin) % 64.49/64.74 True % 64.49/64.74 Clause #4378 (by clausification #[244]): ∀ (a_1 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.74 Or (Eq a b) % 64.49/64.74 (Eq % 64.49/64.74 (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) (skS.0 4 a b a_1) % 64.49/64.74 arrow_1985332922le_Lin) % 64.49/64.74 False) % 64.49/64.74 Clause #4379 (by forward contextual literal cutting #[4378, 116]): ∀ (a_1 : fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool), % 64.49/64.74 Eq % 64.49/64.74 (member (fun (product_prod arrow_411405190le_alt arrow_411405190le_alt) bool) (skS.0 4 a b a_1) % 64.49/64.74 arrow_1985332922le_Lin) % 64.49/64.74 False % 64.49/64.74 Clause #4381 (by superposition #[4379, 2124]): Eq False True % 64.49/64.74 Clause #4409 (by clausification #[4381]): False % 64.49/64.74 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------