%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW553_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.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 08:06:25 PM UTC 2025 % Result : Theorem 4.43s 4.64s % Output : Proof 4.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWW553_5 : TPTP v9.2.0. Released v6.0.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n012.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 11:22:08 EDT 2025 % 0.13/0.34 % CPUTime : % 4.43/4.64 SZS status Theorem for theBenchmark.p % 4.43/4.64 SZS output start Proof for theBenchmark.p % 4.43/4.64 Clause #0 (by assumption #[]): Eq (widen (product_prod (list (list char)) (exp (list char))) p tv tf) True % 4.43/4.64 Clause #1 (by assumption #[]): Eq (Eq (typeof_h ha v) (some ty tv)) True % 4.43/4.64 Clause #5 (by assumption #[]): Eq % 4.43/4.64 (∀ (A : Type) (T4 Ta : ty) (Va : val) % 4.43/4.64 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 4.43/4.64 (Pa : % 4.43/4.64 list % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list (product_prod (list char) ty)) % 4.43/4.64 (list (product_prod (list char) (product_prod (list ty) (product_prod ty A)))))))), % 4.43/4.64 conf A Pa Hb Va Ta → widen A Pa Ta T4 → conf A Pa Hb Va T4) % 4.43/4.64 True % 4.43/4.64 Clause #7 (by assumption #[]): Eq % 4.43/4.64 (∀ (A : Type) % 4.43/4.64 (Pa : % 4.43/4.64 list % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list (product_prod (list char) ty)) % 4.43/4.64 (list (product_prod (list char) (product_prod (list ty) (product_prod ty A)))))))) % 4.43/4.64 (Ta : ty) (Va : val) % 4.43/4.64 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 4.43/4.64 Eq (typeof_h Hb Va) (some ty Ta) → conf A Pa Hb Va Ta) % 4.43/4.64 True % 4.43/4.64 Clause #99 (by assumption #[]): Eq (Not (conf (product_prod (list (list char)) (exp (list char))) p ha v tf)) True % 4.43/4.64 Clause #132 (by clausification #[1]): Eq (typeof_h ha v) (some ty tv) % 4.43/4.64 Clause #217 (by clausification #[5]): ∀ (a : Type), % 4.43/4.64 Eq % 4.43/4.64 (∀ (T4 Ta : ty) (Va : val) % 4.43/4.64 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 4.43/4.64 (Pa : % 4.43/4.64 list % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list (product_prod (list char) ty)) % 4.43/4.64 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 4.43/4.64 conf a Pa Hb Va Ta → widen a Pa Ta T4 → conf a Pa Hb Va T4) % 4.43/4.64 True % 4.43/4.64 Clause #218 (by clausification #[217]): ∀ (a : Type) (a_1 : ty), % 4.43/4.64 Eq % 4.43/4.64 (∀ (Ta : ty) (Va : val) % 4.43/4.64 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 4.43/4.64 (Pa : % 4.43/4.64 list % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list (product_prod (list char) ty)) % 4.43/4.64 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 4.43/4.64 conf a Pa Hb Va Ta → widen a Pa Ta a_1 → conf a Pa Hb Va a_1) % 4.43/4.64 True % 4.43/4.64 Clause #219 (by clausification #[218]): ∀ (a : Type) (a_1 a_2 : ty), % 4.43/4.64 Eq % 4.43/4.64 (∀ (Va : val) % 4.43/4.64 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 4.43/4.64 (Pa : % 4.43/4.64 list % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list (product_prod (list char) ty)) % 4.43/4.64 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 4.43/4.64 conf a Pa Hb Va a_1 → widen a Pa a_1 a_2 → conf a Pa Hb Va a_2) % 4.43/4.64 True % 4.43/4.64 Clause #220 (by clausification #[219]): ∀ (a : Type) (a_1 : val) (a_2 a_3 : ty), % 4.43/4.64 Eq % 4.43/4.64 (∀ (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 4.43/4.64 (Pa : % 4.43/4.64 list % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list (product_prod (list char) ty)) % 4.43/4.64 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 4.43/4.64 conf a Pa Hb a_1 a_2 → widen a Pa a_2 a_3 → conf a Pa Hb a_1 a_3) % 4.43/4.64 True % 4.43/4.64 Clause #221 (by clausification #[220]): ∀ (a : Type) % 4.43/4.64 (a_1 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 4.43/4.64 (a_2 : val) (a_3 a_4 : ty), % 4.43/4.64 Eq % 4.43/4.64 (∀ % 4.43/4.64 (Pa : % 4.43/4.64 list % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list char) % 4.43/4.64 (product_prod (list (product_prod (list char) ty)) % 4.43/4.64 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 4.43/4.66 conf a Pa a_1 a_2 a_3 → widen a Pa a_3 a_4 → conf a Pa a_1 a_2 a_4) % 4.43/4.66 True % 4.43/4.66 Clause #222 (by clausification #[221]): ∀ (a : Type) % 4.43/4.66 (a_1 : % 4.43/4.66 list % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list (product_prod (list char) ty)) % 4.43/4.66 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))) % 4.43/4.66 (a_2 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 4.43/4.66 (a_3 : val) (a_4 a_5 : ty), Eq (conf a a_1 a_2 a_3 a_4 → widen a a_1 a_4 a_5 → conf a a_1 a_2 a_3 a_5) True % 4.43/4.66 Clause #223 (by clausification #[222]): ∀ (a : Type) % 4.43/4.66 (a_1 : % 4.43/4.66 list % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list (product_prod (list char) ty)) % 4.43/4.66 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))) % 4.43/4.66 (a_2 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 4.43/4.66 (a_3 : val) (a_4 a_5 : ty), % 4.43/4.66 Or (Eq (conf a a_1 a_2 a_3 a_4) False) (Eq (widen a a_1 a_4 a_5 → conf a a_1 a_2 a_3 a_5) True) % 4.43/4.66 Clause #224 (by clausification #[223]): ∀ (a : Type) % 4.43/4.66 (a_1 : % 4.43/4.66 list % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list (product_prod (list char) ty)) % 4.43/4.66 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))) % 4.43/4.66 (a_2 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 4.43/4.66 (a_3 : val) (a_4 a_5 : ty), % 4.43/4.66 Or (Eq (conf a a_1 a_2 a_3 a_4) False) (Or (Eq (widen a a_1 a_4 a_5) False) (Eq (conf a a_1 a_2 a_3 a_5) True)) % 4.43/4.66 Clause #253 (by clausification #[7]): ∀ (a : Type), % 4.43/4.66 Eq % 4.43/4.66 (∀ % 4.43/4.66 (Pa : % 4.43/4.66 list % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list (product_prod (list char) ty)) % 4.43/4.66 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))) % 4.43/4.66 (Ta : ty) (Va : val) % 4.43/4.66 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 4.43/4.66 Eq (typeof_h Hb Va) (some ty Ta) → conf a Pa Hb Va Ta) % 4.43/4.66 True % 4.43/4.66 Clause #254 (by clausification #[253]): ∀ (a : Type) % 4.43/4.66 (a_1 : % 4.43/4.66 list % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list (product_prod (list char) ty)) % 4.43/4.66 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 4.43/4.66 Eq % 4.43/4.66 (∀ (Ta : ty) (Va : val) % 4.43/4.66 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 4.43/4.66 Eq (typeof_h Hb Va) (some ty Ta) → conf a a_1 Hb Va Ta) % 4.43/4.66 True % 4.43/4.66 Clause #255 (by clausification #[254]): ∀ (a : ty) (a_1 : Type) % 4.43/4.66 (a_2 : % 4.43/4.66 list % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list (product_prod (list char) ty)) % 4.43/4.66 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a_1)))))))), % 4.43/4.66 Eq % 4.43/4.66 (∀ (Va : val) % 4.43/4.66 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 4.43/4.66 Eq (typeof_h Hb Va) (some ty a) → conf a_1 a_2 Hb Va a) % 4.43/4.66 True % 4.43/4.66 Clause #256 (by clausification #[255]): ∀ (a : val) (a_1 : ty) (a_2 : Type) % 4.43/4.66 (a_3 : % 4.43/4.66 list % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list char) % 4.43/4.66 (product_prod (list (product_prod (list char) ty)) % 4.43/4.66 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a_2)))))))), % 4.43/4.66 Eq % 4.43/4.66 (∀ (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 4.43/4.66 Eq (typeof_h Hb a) (some ty a_1) → conf a_2 a_3 Hb a a_1) % 4.43/4.66 True % 4.43/4.66 Clause #257 (by clausification #[256]): ∀ (a : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 4.43/4.66 (a_1 : val) (a_2 : ty) (a_3 : Type) % 4.43/4.66 (a_4 : % 4.43/4.66 list % 4.43/4.66 (product_prod (list char) % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list (product_prod (list char) ty)) % 4.43/4.68 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a_3)))))))), % 4.43/4.68 Eq (Eq (typeof_h a a_1) (some ty a_2) → conf a_3 a_4 a a_1 a_2) True % 4.43/4.68 Clause #258 (by clausification #[257]): ∀ (a : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 4.43/4.68 (a_1 : val) (a_2 : ty) (a_3 : Type) % 4.43/4.68 (a_4 : % 4.43/4.68 list % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list (product_prod (list char) ty)) % 4.43/4.68 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a_3)))))))), % 4.43/4.68 Or (Eq (Eq (typeof_h a a_1) (some ty a_2)) False) (Eq (conf a_3 a_4 a a_1 a_2) True) % 4.43/4.68 Clause #259 (by clausification #[258]): ∀ (a : Type) % 4.43/4.68 (a_1 : % 4.43/4.68 list % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list (product_prod (list char) ty)) % 4.43/4.68 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))) % 4.43/4.68 (a_2 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 4.43/4.68 (a_3 : val) (a_4 : ty), Or (Eq (conf a a_1 a_2 a_3 a_4) True) (Ne (typeof_h a_2 a_3) (some ty a_4)) % 4.43/4.68 Clause #260 (by superposition #[259, 132]): ∀ (a : Type) % 4.43/4.68 (a_1 : % 4.43/4.68 list % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list (product_prod (list char) ty)) % 4.43/4.68 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))) % 4.43/4.68 (a_2 : ty), Or (Eq (conf a a_1 ha v a_2) True) (Ne (some ty tv) (some ty a_2)) % 4.43/4.68 Clause #263 (by equality resolution #[260]): ∀ (a : Type) % 4.43/4.68 (a_1 : % 4.43/4.68 list % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list (product_prod (list char) ty)) % 4.43/4.68 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 4.43/4.68 Eq (conf a a_1 ha v tv) True % 4.43/4.68 Clause #267 (by superposition #[263, 224]): ∀ (a : Type) % 4.43/4.68 (a_1 : % 4.43/4.68 list % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list (product_prod (list char) ty)) % 4.43/4.68 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))) % 4.43/4.68 (a_2 : ty), Or (Eq True False) (Or (Eq (widen a a_1 tv a_2) False) (Eq (conf a a_1 ha v a_2) True)) % 4.43/4.68 Clause #296 (by clausification #[99]): Eq (conf (product_prod (list (list char)) (exp (list char))) p ha v tf) False % 4.43/4.68 Clause #368 (by clausification #[267]): ∀ (a : Type) % 4.43/4.68 (a_1 : % 4.43/4.68 list % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list char) % 4.43/4.68 (product_prod (list (product_prod (list char) ty)) % 4.43/4.68 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))) % 4.43/4.68 (a_2 : ty), Or (Eq (widen a a_1 tv a_2) False) (Eq (conf a a_1 ha v a_2) True) % 4.43/4.68 Clause #369 (by superposition #[368, 0]): Or (Eq (conf (product_prod (list (list char)) (exp (list char))) p ha v tf) True) (Eq False True) % 4.43/4.68 Clause #371 (by clausification #[369]): Eq (conf (product_prod (list (list char)) (exp (list char))) p ha v tf) True % 4.43/4.68 Clause #372 (by superposition #[371, 296]): Eq True False % 4.43/4.68 Clause #374 (by clausification #[372]): False % 4.43/4.68 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------