%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW568_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 48.45s 48.65s % Output : Proof 48.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.13 % Problem : SWW568_5 : TPTP v9.2.0. Released v6.0.0. % 0.06/0.14 % Command : duper %s % 0.14/0.35 % Computer : n006.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Oct 2 10:25:23 EDT 2025 % 0.14/0.35 % CPUTime : % 48.45/48.65 SZS status Theorem for theBenchmark.p % 48.45/48.65 SZS output start Proof for theBenchmark.p % 48.45/48.65 Clause #0 (by assumption #[]): Eq (wTrt p h_a e e_a u) True % 48.45/48.65 Clause #4 (by assumption #[]): Eq % 48.45/48.65 (∀ (M : Type) (T1 : ty) % 48.45/48.65 (P2 : % 48.45/48.65 list % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list (product_prod (list char) ty)) % 48.45/48.65 (list (product_prod (list char) (product_prod (list ty) (product_prod ty M)))))))), % 48.45/48.65 widen M P2 T1 T1) % 48.45/48.65 True % 48.45/48.65 Clause #9 (by assumption #[]): Eq % 48.45/48.65 (∀ (Ta : ty) (Da Fa : list char) (Eb : exp (list char)) (Ea : fun (list char) (option ty)) % 48.45/48.65 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 48.45/48.65 (Pa : % 48.45/48.65 list % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list (product_prod (list char) ty)) % 48.45/48.65 (list % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 48.45/48.65 wTrt Pa Hb Ea Eb nt → wTrt Pa Hb Ea (fAcc (list char) Eb Fa Da) Ta) % 48.45/48.65 True % 48.45/48.65 Clause #12 (by assumption #[]): Eq (Eq u nt) True % 48.45/48.65 Clause #98 (by assumption #[]): Eq % 48.45/48.65 (Not % 48.45/48.65 (Exists fun T => % 48.45/48.65 And (wTrt p h_a e (fAcc (list char) e_a f d) T) % 48.45/48.65 (widen (product_prod (list (list char)) (exp (list char))) p T t))) % 48.45/48.65 True % 48.45/48.65 Clause #101 (by clausification #[12]): Eq u nt % 48.45/48.65 Clause #102 (by forward demodulation #[0, 101]): Eq (wTrt p h_a e e_a nt) True % 48.45/48.65 Clause #107 (by clausification #[4]): ∀ (a : Type), % 48.45/48.65 Eq % 48.45/48.65 (∀ (T1 : ty) % 48.45/48.65 (P2 : % 48.45/48.65 list % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list (product_prod (list char) ty)) % 48.45/48.65 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 48.45/48.65 widen a P2 T1 T1) % 48.45/48.65 True % 48.45/48.65 Clause #108 (by clausification #[107]): ∀ (a : Type) (a_1 : ty), % 48.45/48.65 Eq % 48.45/48.65 (∀ % 48.45/48.65 (P2 : % 48.45/48.65 list % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list (product_prod (list char) ty)) % 48.45/48.65 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 48.45/48.65 widen a P2 a_1 a_1) % 48.45/48.65 True % 48.45/48.65 Clause #109 (by clausification #[108]): ∀ (a : Type) % 48.45/48.65 (a_1 : % 48.45/48.65 list % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list (product_prod (list char) ty)) % 48.45/48.65 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))) % 48.45/48.65 (a_2 : ty), Eq (widen a a_1 a_2 a_2) True % 48.45/48.65 Clause #242 (by clausification #[9]): ∀ (a : ty), % 48.45/48.65 Eq % 48.45/48.65 (∀ (Da Fa : list char) (Eb : exp (list char)) (Ea : fun (list char) (option ty)) % 48.45/48.65 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 48.45/48.65 (Pa : % 48.45/48.65 list % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list (product_prod (list char) ty)) % 48.45/48.65 (list % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list ty) % 48.45/48.65 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 48.45/48.65 wTrt Pa Hb Ea Eb nt → wTrt Pa Hb Ea (fAcc (list char) Eb Fa Da) a) % 48.45/48.65 True % 48.45/48.65 Clause #243 (by clausification #[242]): ∀ (a : list char) (a_1 : ty), % 48.45/48.65 Eq % 48.45/48.65 (∀ (Fa : list char) (Eb : exp (list char)) (Ea : fun (list char) (option ty)) % 48.45/48.65 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 48.45/48.65 (Pa : % 48.45/48.65 list % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list (product_prod (list char) ty)) % 48.45/48.65 (list % 48.45/48.65 (product_prod (list char) % 48.45/48.65 (product_prod (list ty) % 48.45/48.65 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 48.45/48.65 wTrt Pa Hb Ea Eb nt → wTrt Pa Hb Ea (fAcc (list char) Eb Fa a) a_1) % 48.45/48.65 True % 48.45/48.65 Clause #244 (by clausification #[243]): ∀ (a a_1 : list char) (a_2 : ty), % 48.50/48.66 Eq % 48.50/48.66 (∀ (Eb : exp (list char)) (Ea : fun (list char) (option ty)) % 48.50/48.66 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 48.50/48.66 (Pa : % 48.50/48.66 list % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list (product_prod (list char) ty)) % 48.50/48.66 (list % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list ty) % 48.50/48.66 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 48.50/48.66 wTrt Pa Hb Ea Eb nt → wTrt Pa Hb Ea (fAcc (list char) Eb a a_1) a_2) % 48.50/48.66 True % 48.50/48.66 Clause #245 (by clausification #[244]): ∀ (a : exp (list char)) (a_1 a_2 : list char) (a_3 : ty), % 48.50/48.66 Eq % 48.50/48.66 (∀ (Ea : fun (list char) (option ty)) % 48.50/48.66 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 48.50/48.66 (Pa : % 48.50/48.66 list % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list (product_prod (list char) ty)) % 48.50/48.66 (list % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list ty) % 48.50/48.66 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 48.50/48.66 wTrt Pa Hb Ea a nt → wTrt Pa Hb Ea (fAcc (list char) a a_1 a_2) a_3) % 48.50/48.66 True % 48.50/48.66 Clause #246 (by clausification #[245]): ∀ (a : fun (list char) (option ty)) (a_1 : exp (list char)) (a_2 a_3 : list char) (a_4 : ty), % 48.50/48.66 Eq % 48.50/48.66 (∀ (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 48.50/48.66 (Pa : % 48.50/48.66 list % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list (product_prod (list char) ty)) % 48.50/48.66 (list % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list ty) % 48.50/48.66 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 48.50/48.66 wTrt Pa Hb a a_1 nt → wTrt Pa Hb a (fAcc (list char) a_1 a_2 a_3) a_4) % 48.50/48.66 True % 48.50/48.66 Clause #247 (by clausification #[246]): ∀ (a : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 48.50/48.66 (a_1 : fun (list char) (option ty)) (a_2 : exp (list char)) (a_3 a_4 : list char) (a_5 : ty), % 48.50/48.66 Eq % 48.50/48.66 (∀ % 48.50/48.66 (Pa : % 48.50/48.66 list % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list (product_prod (list char) ty)) % 48.50/48.66 (list % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list ty) % 48.50/48.66 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 48.50/48.66 wTrt Pa a a_1 a_2 nt → wTrt Pa a a_1 (fAcc (list char) a_2 a_3 a_4) a_5) % 48.50/48.66 True % 48.50/48.66 Clause #248 (by clausification #[247]): ∀ % 48.50/48.66 (a : % 48.50/48.66 list % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list (product_prod (list char) ty)) % 48.50/48.66 (list % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))) % 48.50/48.66 (a_1 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 48.50/48.66 (a_2 : fun (list char) (option ty)) (a_3 : exp (list char)) (a_4 a_5 : list char) (a_6 : ty), % 48.50/48.66 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 % 48.50/48.66 Clause #249 (by clausification #[248]): ∀ % 48.50/48.66 (a : % 48.50/48.66 list % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list (product_prod (list char) ty)) % 48.50/48.66 (list % 48.50/48.66 (product_prod (list char) % 48.50/48.66 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))) % 48.50/48.66 (a_1 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 48.50/48.66 (a_2 : fun (list char) (option ty)) (a_3 : exp (list char)) (a_4 a_5 : list char) (a_6 : ty), % 48.50/48.66 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) % 48.50/48.68 Clause #250 (by superposition #[249, 102]): ∀ (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) % 48.50/48.68 Clause #251 (by clausification #[250]): ∀ (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 % 48.50/48.68 Clause #1651 (by clausification #[98]): Eq % 48.50/48.68 (Exists fun T => % 48.50/48.68 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)) % 48.50/48.68 False % 48.50/48.68 Clause #1652 (by clausification #[1651]): ∀ (a : ty), % 48.50/48.68 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)) % 48.50/48.68 False % 48.50/48.68 Clause #1653 (by clausification #[1652]): ∀ (a : ty), % 48.50/48.68 Or (Eq (wTrt p h_a e (fAcc (list char) e_a f d) a) False) % 48.50/48.68 (Eq (widen (product_prod (list (list char)) (exp (list char))) p a t) False) % 48.50/48.68 Clause #1654 (by superposition #[1653, 251]): ∀ (a : ty), Or (Eq (widen (product_prod (list (list char)) (exp (list char))) p a t) False) (Eq False True) % 48.50/48.68 Clause #1655 (by clausification #[1654]): ∀ (a : ty), Eq (widen (product_prod (list (list char)) (exp (list char))) p a t) False % 48.50/48.68 Clause #1657 (by superposition #[1655, 109]): Eq False True % 48.50/48.68 Clause #1658 (by clausification #[1657]): False % 48.50/48.68 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------