%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW569_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n006.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:26 PM UTC 2025 % Result : Theorem 45.27s 45.48s % Output : Proof 45.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWW569_5 : TPTP v9.2.0. Released v6.0.0. % 0.03/0.13 % Command : duper %s % 0.13/0.34 % Computer : n006.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:16:38 EDT 2025 % 0.13/0.35 % CPUTime : % 45.27/45.48 SZS status Theorem for theBenchmark.p % 45.27/45.48 SZS output start Proof for theBenchmark.p % 45.27/45.48 Clause #0 (by assumption #[]): Eq (wTrt p h_a e e_a nt) True % 45.27/45.48 Clause #3 (by assumption #[]): Eq % 45.27/45.48 (∀ (M : Type) (T1 : ty) % 45.27/45.48 (P2 : % 45.27/45.48 list % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list (product_prod (list char) ty)) % 45.27/45.48 (list (product_prod (list char) (product_prod (list ty) (product_prod ty M)))))))), % 45.27/45.48 widen M P2 T1 T1) % 45.27/45.48 True % 45.27/45.48 Clause #7 (by assumption #[]): Eq % 45.27/45.48 (∀ (Ta : ty) (Da Fa : list char) (Eb : exp (list char)) (Ea : fun (list char) (option ty)) % 45.27/45.48 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 45.27/45.48 (Pa : % 45.27/45.48 list % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list (product_prod (list char) ty)) % 45.27/45.48 (list % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 45.27/45.48 wTrt Pa Hb Ea Eb nt → wTrt Pa Hb Ea (fAcc (list char) Eb Fa Da) Ta) % 45.27/45.48 True % 45.27/45.48 Clause #97 (by assumption #[]): Eq % 45.27/45.48 (Not % 45.27/45.48 (Exists fun T => % 45.27/45.48 And (wTrt p h_a e (fAcc (list char) e_a f d) T) % 45.27/45.48 (widen (product_prod (list (list char)) (exp (list char))) p T t))) % 45.27/45.48 True % 45.27/45.48 Clause #104 (by clausification #[3]): ∀ (a : Type), % 45.27/45.48 Eq % 45.27/45.48 (∀ (T1 : ty) % 45.27/45.48 (P2 : % 45.27/45.48 list % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list (product_prod (list char) ty)) % 45.27/45.48 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 45.27/45.48 widen a P2 T1 T1) % 45.27/45.48 True % 45.27/45.48 Clause #105 (by clausification #[104]): ∀ (a : Type) (a_1 : ty), % 45.27/45.48 Eq % 45.27/45.48 (∀ % 45.27/45.48 (P2 : % 45.27/45.48 list % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list (product_prod (list char) ty)) % 45.27/45.48 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 45.27/45.48 widen a P2 a_1 a_1) % 45.27/45.48 True % 45.27/45.48 Clause #106 (by clausification #[105]): ∀ (a : Type) % 45.27/45.48 (a_1 : % 45.27/45.48 list % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list (product_prod (list char) ty)) % 45.27/45.48 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))) % 45.27/45.48 (a_2 : ty), Eq (widen a a_1 a_2 a_2) True % 45.27/45.48 Clause #224 (by clausification #[7]): ∀ (a : ty), % 45.27/45.48 Eq % 45.27/45.48 (∀ (Da Fa : list char) (Eb : exp (list char)) (Ea : fun (list char) (option ty)) % 45.27/45.48 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 45.27/45.48 (Pa : % 45.27/45.48 list % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list (product_prod (list char) ty)) % 45.27/45.48 (list % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list ty) % 45.27/45.48 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 45.27/45.48 wTrt Pa Hb Ea Eb nt → wTrt Pa Hb Ea (fAcc (list char) Eb Fa Da) a) % 45.27/45.48 True % 45.27/45.48 Clause #225 (by clausification #[224]): ∀ (a : list char) (a_1 : ty), % 45.27/45.48 Eq % 45.27/45.48 (∀ (Fa : list char) (Eb : exp (list char)) (Ea : fun (list char) (option ty)) % 45.27/45.48 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 45.27/45.48 (Pa : % 45.27/45.48 list % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list (product_prod (list char) ty)) % 45.27/45.48 (list % 45.27/45.48 (product_prod (list char) % 45.27/45.48 (product_prod (list ty) % 45.27/45.48 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 45.27/45.48 wTrt Pa Hb Ea Eb nt → wTrt Pa Hb Ea (fAcc (list char) Eb Fa a) a_1) % 45.27/45.48 True % 45.27/45.48 Clause #226 (by clausification #[225]): ∀ (a a_1 : list char) (a_2 : ty), % 45.27/45.48 Eq % 45.27/45.48 (∀ (Eb : exp (list char)) (Ea : fun (list char) (option ty)) % 45.27/45.48 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 45.27/45.50 (Pa : % 45.27/45.50 list % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list (product_prod (list char) ty)) % 45.27/45.50 (list % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list ty) % 45.27/45.50 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 45.27/45.50 wTrt Pa Hb Ea Eb nt → wTrt Pa Hb Ea (fAcc (list char) Eb a a_1) a_2) % 45.27/45.50 True % 45.27/45.50 Clause #227 (by clausification #[226]): ∀ (a : exp (list char)) (a_1 a_2 : list char) (a_3 : ty), % 45.27/45.50 Eq % 45.27/45.50 (∀ (Ea : fun (list char) (option ty)) % 45.27/45.50 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 45.27/45.50 (Pa : % 45.27/45.50 list % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list (product_prod (list char) ty)) % 45.27/45.50 (list % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list ty) % 45.27/45.50 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 45.27/45.50 wTrt Pa Hb Ea a nt → wTrt Pa Hb Ea (fAcc (list char) a a_1 a_2) a_3) % 45.27/45.50 True % 45.27/45.50 Clause #228 (by clausification #[227]): ∀ (a : fun (list char) (option ty)) (a_1 : exp (list char)) (a_2 a_3 : list char) (a_4 : ty), % 45.27/45.50 Eq % 45.27/45.50 (∀ (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 45.27/45.50 (Pa : % 45.27/45.50 list % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list (product_prod (list char) ty)) % 45.27/45.50 (list % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list ty) % 45.27/45.50 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 45.27/45.50 wTrt Pa Hb a a_1 nt → wTrt Pa Hb a (fAcc (list char) a_1 a_2 a_3) a_4) % 45.27/45.50 True % 45.27/45.50 Clause #229 (by clausification #[228]): ∀ (a : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 45.27/45.50 (a_1 : fun (list char) (option ty)) (a_2 : exp (list char)) (a_3 a_4 : list char) (a_5 : ty), % 45.27/45.50 Eq % 45.27/45.50 (∀ % 45.27/45.50 (Pa : % 45.27/45.50 list % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list (product_prod (list char) ty)) % 45.27/45.50 (list % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list ty) % 45.27/45.50 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 45.27/45.50 wTrt Pa a a_1 a_2 nt → wTrt Pa a a_1 (fAcc (list char) a_2 a_3 a_4) a_5) % 45.27/45.50 True % 45.27/45.50 Clause #230 (by clausification #[229]): ∀ % 45.27/45.50 (a : % 45.27/45.50 list % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list (product_prod (list char) ty)) % 45.27/45.50 (list % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))) % 45.27/45.50 (a_1 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 45.27/45.50 (a_2 : fun (list char) (option ty)) (a_3 : exp (list char)) (a_4 a_5 : list char) (a_6 : ty), % 45.27/45.50 Eq (wTrt a a_1 a_2 a_3 nt → wTrt a a_1 a_2 (fAcc (list char) a_3 a_4 a_5) a_6) True % 45.27/45.50 Clause #231 (by clausification #[230]): ∀ % 45.27/45.50 (a : % 45.27/45.50 list % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list (product_prod (list char) ty)) % 45.27/45.50 (list % 45.27/45.50 (product_prod (list char) % 45.27/45.50 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))) % 45.27/45.50 (a_1 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 45.27/45.50 (a_2 : fun (list char) (option ty)) (a_3 : exp (list char)) (a_4 a_5 : list char) (a_6 : ty), % 45.27/45.50 Or (Eq (wTrt a a_1 a_2 a_3 nt) False) (Eq (wTrt a a_1 a_2 (fAcc (list char) a_3 a_4 a_5) a_6) True) % 45.27/45.50 Clause #232 (by superposition #[231, 0]): ∀ (a a_1 : list char) (a_2 : ty), Or (Eq (wTrt p h_a e (fAcc (list char) e_a a a_1) a_2) True) (Eq False True) % 45.35/45.52 Clause #234 (by clausification #[232]): ∀ (a a_1 : list char) (a_2 : ty), Eq (wTrt p h_a e (fAcc (list char) e_a a a_1) a_2) True % 45.35/45.52 Clause #1731 (by clausification #[97]): Eq % 45.35/45.52 (Exists fun T => % 45.35/45.52 And (wTrt p h_a e (fAcc (list char) e_a f d) T) (widen (product_prod (list (list char)) (exp (list char))) p T t)) % 45.35/45.52 False % 45.35/45.52 Clause #1732 (by clausification #[1731]): ∀ (a : ty), % 45.35/45.52 Eq (And (wTrt p h_a e (fAcc (list char) e_a f d) a) (widen (product_prod (list (list char)) (exp (list char))) p a t)) % 45.35/45.52 False % 45.35/45.52 Clause #1733 (by clausification #[1732]): ∀ (a : ty), % 45.35/45.52 Or (Eq (wTrt p h_a e (fAcc (list char) e_a f d) a) False) % 45.35/45.52 (Eq (widen (product_prod (list (list char)) (exp (list char))) p a t) False) % 45.35/45.52 Clause #1734 (by superposition #[1733, 234]): ∀ (a : ty), Or (Eq (widen (product_prod (list (list char)) (exp (list char))) p a t) False) (Eq False True) % 45.35/45.52 Clause #1735 (by clausification #[1734]): ∀ (a : ty), Eq (widen (product_prod (list (list char)) (exp (list char))) p a t) False % 45.35/45.52 Clause #1737 (by superposition #[1735, 106]): Eq False True % 45.35/45.52 Clause #1738 (by clausification #[1737]): False % 45.35/45.52 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------