%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW571_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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:27 PM UTC 2025 % Result : Theorem 44.81s 45.04s % Output : Proof 44.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.13 % Problem : SWW571_5 : TPTP v9.2.0. Released v6.0.0. % 0.06/0.14 % Command : duper %s % 0.14/0.35 % Computer : n007.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 11:05:53 EDT 2025 % 0.14/0.35 % CPUTime : % 44.81/45.04 SZS status Theorem for theBenchmark.p % 44.81/45.04 SZS output start Proof for theBenchmark.p % 44.81/45.04 Clause #0 (by assumption #[]): Eq (Eq t void) True % 44.81/45.04 Clause #1 (by assumption #[]): Eq (wTrt p h_a e e_2 t_2) True % 44.81/45.04 Clause #2 (by assumption #[]): Eq (wTrt p h_a e e_a nt) True % 44.81/45.04 Clause #7 (by assumption #[]): Eq % 44.81/45.04 (∀ (M : Type) (T2 : ty) % 44.81/45.04 (P2 : % 44.81/45.04 list % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list (product_prod (list char) ty)) % 44.81/45.04 (list (product_prod (list char) (product_prod (list ty) (product_prod ty M)))))))), % 44.81/45.04 widen M P2 T2 T2) % 44.81/45.04 True % 44.81/45.04 Clause #11 (by assumption #[]): Eq % 44.81/45.04 (∀ (Da Fa : list char) (T_2 : ty) (E_2 E_1 : exp (list char)) (Ea : fun (list char) (option ty)) % 44.81/45.04 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 44.81/45.04 (Pa : % 44.81/45.04 list % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list (product_prod (list char) ty)) % 44.81/45.04 (list % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 44.81/45.04 wTrt Pa Hb Ea E_1 nt → wTrt Pa Hb Ea E_2 T_2 → wTrt Pa Hb Ea (fAss (list char) E_1 Fa Da E_2) void) % 44.81/45.04 True % 44.81/45.04 Clause #98 (by assumption #[]): Eq % 44.81/45.04 (Not % 44.81/45.04 (Exists fun T => % 44.81/45.04 And (wTrt p h_a e (fAss (list char) e_a f d e_2) T) % 44.81/45.04 (widen (product_prod (list (list char)) (exp (list char))) p T t))) % 44.81/45.04 True % 44.81/45.04 Clause #102 (by clausification #[0]): Eq t void % 44.81/45.04 Clause #105 (by clausification #[7]): ∀ (a : Type), % 44.81/45.04 Eq % 44.81/45.04 (∀ (T2 : ty) % 44.81/45.04 (P2 : % 44.81/45.04 list % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list (product_prod (list char) ty)) % 44.81/45.04 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 44.81/45.04 widen a P2 T2 T2) % 44.81/45.04 True % 44.81/45.04 Clause #106 (by clausification #[105]): ∀ (a : Type) (a_1 : ty), % 44.81/45.04 Eq % 44.81/45.04 (∀ % 44.81/45.04 (P2 : % 44.81/45.04 list % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list (product_prod (list char) ty)) % 44.81/45.04 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))), % 44.81/45.04 widen a P2 a_1 a_1) % 44.81/45.04 True % 44.81/45.04 Clause #107 (by clausification #[106]): ∀ (a : Type) % 44.81/45.04 (a_1 : % 44.81/45.04 list % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list (product_prod (list char) ty)) % 44.81/45.04 (list (product_prod (list char) (product_prod (list ty) (product_prod ty a)))))))) % 44.81/45.04 (a_2 : ty), Eq (widen a a_1 a_2 a_2) True % 44.81/45.04 Clause #165 (by clausification #[11]): ∀ (a : list char), % 44.81/45.04 Eq % 44.81/45.04 (∀ (Fa : list char) (T_2 : ty) (E_2 E_1 : exp (list char)) (Ea : fun (list char) (option ty)) % 44.81/45.04 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 44.81/45.04 (Pa : % 44.81/45.04 list % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list (product_prod (list char) ty)) % 44.81/45.04 (list % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list ty) % 44.81/45.04 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 44.81/45.04 wTrt Pa Hb Ea E_1 nt → wTrt Pa Hb Ea E_2 T_2 → wTrt Pa Hb Ea (fAss (list char) E_1 Fa a E_2) void) % 44.81/45.04 True % 44.81/45.04 Clause #166 (by clausification #[165]): ∀ (a a_1 : list char), % 44.81/45.04 Eq % 44.81/45.04 (∀ (T_2 : ty) (E_2 E_1 : exp (list char)) (Ea : fun (list char) (option ty)) % 44.81/45.04 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 44.81/45.04 (Pa : % 44.81/45.04 list % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list (product_prod (list char) ty)) % 44.81/45.04 (list % 44.81/45.04 (product_prod (list char) % 44.81/45.04 (product_prod (list ty) % 44.81/45.04 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 44.81/45.04 wTrt Pa Hb Ea E_1 nt → wTrt Pa Hb Ea E_2 T_2 → wTrt Pa Hb Ea (fAss (list char) E_1 a a_1 E_2) void) % 44.81/45.06 True % 44.81/45.06 Clause #167 (by clausification #[166]): ∀ (a : ty) (a_1 a_2 : list char), % 44.81/45.06 Eq % 44.81/45.06 (∀ (E_2 E_1 : exp (list char)) (Ea : fun (list char) (option ty)) % 44.81/45.06 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 44.81/45.06 (Pa : % 44.81/45.06 list % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list (product_prod (list char) ty)) % 44.81/45.06 (list % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list ty) % 44.81/45.06 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 44.81/45.06 wTrt Pa Hb Ea E_1 nt → wTrt Pa Hb Ea E_2 a → wTrt Pa Hb Ea (fAss (list char) E_1 a_1 a_2 E_2) void) % 44.81/45.06 True % 44.81/45.06 Clause #168 (by clausification #[167]): ∀ (a : exp (list char)) (a_1 : ty) (a_2 a_3 : list char), % 44.81/45.06 Eq % 44.81/45.06 (∀ (E_1 : exp (list char)) (Ea : fun (list char) (option ty)) % 44.81/45.06 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 44.81/45.06 (Pa : % 44.81/45.06 list % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list (product_prod (list char) ty)) % 44.81/45.06 (list % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list ty) % 44.81/45.06 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 44.81/45.06 wTrt Pa Hb Ea E_1 nt → wTrt Pa Hb Ea a a_1 → wTrt Pa Hb Ea (fAss (list char) E_1 a_2 a_3 a) void) % 44.81/45.06 True % 44.81/45.06 Clause #169 (by clausification #[168]): ∀ (a a_1 : exp (list char)) (a_2 : ty) (a_3 a_4 : list char), % 44.81/45.06 Eq % 44.81/45.06 (∀ (Ea : fun (list char) (option ty)) % 44.81/45.06 (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 44.81/45.06 (Pa : % 44.81/45.06 list % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list (product_prod (list char) ty)) % 44.81/45.06 (list % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list ty) % 44.81/45.06 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 44.81/45.06 wTrt Pa Hb Ea a nt → wTrt Pa Hb Ea a_1 a_2 → wTrt Pa Hb Ea (fAss (list char) a a_3 a_4 a_1) void) % 44.81/45.06 True % 44.81/45.06 Clause #170 (by clausification #[169]): ∀ (a : fun (list char) (option ty)) (a_1 a_2 : exp (list char)) (a_3 : ty) (a_4 a_5 : list char), % 44.81/45.06 Eq % 44.81/45.06 (∀ (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 44.81/45.06 (Pa : % 44.81/45.06 list % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list (product_prod (list char) ty)) % 44.81/45.06 (list % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list ty) % 44.81/45.06 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 44.81/45.06 wTrt Pa Hb a a_1 nt → wTrt Pa Hb a a_2 a_3 → wTrt Pa Hb a (fAss (list char) a_1 a_4 a_5 a_2) void) % 44.81/45.06 True % 44.81/45.06 Clause #171 (by clausification #[170]): ∀ (a : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 44.81/45.06 (a_1 : fun (list char) (option ty)) (a_2 a_3 : exp (list char)) (a_4 : ty) (a_5 a_6 : list char), % 44.81/45.06 Eq % 44.81/45.06 (∀ % 44.81/45.06 (Pa : % 44.81/45.06 list % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list (product_prod (list char) ty)) % 44.81/45.06 (list % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list ty) % 44.81/45.06 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 44.81/45.06 wTrt Pa a a_1 a_2 nt → wTrt Pa a a_1 a_3 a_4 → wTrt Pa a a_1 (fAss (list char) a_2 a_5 a_6 a_3) void) % 44.81/45.06 True % 44.81/45.06 Clause #172 (by clausification #[171]): ∀ % 44.81/45.06 (a : % 44.81/45.06 list % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list char) % 44.81/45.06 (product_prod (list (product_prod (list char) ty)) % 44.81/45.06 (list % 44.91/45.09 (product_prod (list char) % 44.91/45.09 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))) % 44.91/45.09 (a_1 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 44.91/45.09 (a_2 : fun (list char) (option ty)) (a_3 a_4 : exp (list char)) (a_5 : ty) (a_6 a_7 : list char), % 44.91/45.09 Eq (wTrt a a_1 a_2 a_3 nt → wTrt a a_1 a_2 a_4 a_5 → wTrt a a_1 a_2 (fAss (list char) a_3 a_6 a_7 a_4) void) True % 44.91/45.09 Clause #173 (by clausification #[172]): ∀ % 44.91/45.09 (a : % 44.91/45.09 list % 44.91/45.09 (product_prod (list char) % 44.91/45.09 (product_prod (list char) % 44.91/45.09 (product_prod (list (product_prod (list char) ty)) % 44.91/45.09 (list % 44.91/45.09 (product_prod (list char) % 44.91/45.09 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))) % 44.91/45.09 (a_1 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 44.91/45.09 (a_2 : fun (list char) (option ty)) (a_3 a_4 : exp (list char)) (a_5 : ty) (a_6 a_7 : list char), % 44.91/45.09 Or (Eq (wTrt a a_1 a_2 a_3 nt) False) % 44.91/45.09 (Eq (wTrt a a_1 a_2 a_4 a_5 → wTrt a a_1 a_2 (fAss (list char) a_3 a_6 a_7 a_4) void) True) % 44.91/45.09 Clause #174 (by clausification #[173]): ∀ % 44.91/45.09 (a : % 44.91/45.09 list % 44.91/45.09 (product_prod (list char) % 44.91/45.09 (product_prod (list char) % 44.91/45.09 (product_prod (list (product_prod (list char) ty)) % 44.91/45.09 (list % 44.91/45.09 (product_prod (list char) % 44.91/45.09 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))) % 44.91/45.09 (a_1 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 44.91/45.09 (a_2 : fun (list char) (option ty)) (a_3 a_4 : exp (list char)) (a_5 : ty) (a_6 a_7 : list char), % 44.91/45.09 Or (Eq (wTrt a a_1 a_2 a_3 nt) False) % 44.91/45.09 (Or (Eq (wTrt a a_1 a_2 a_4 a_5) False) (Eq (wTrt a a_1 a_2 (fAss (list char) a_3 a_6 a_7 a_4) void) True)) % 44.91/45.09 Clause #175 (by superposition #[174, 2]): ∀ (a : exp (list char)) (a_1 : ty) (a_2 a_3 : list char), % 44.91/45.09 Or (Eq (wTrt p h_a e a a_1) False) (Or (Eq (wTrt p h_a e (fAss (list char) e_a a_2 a_3 a) void) True) (Eq False True)) % 44.91/45.09 Clause #782 (by clausification #[175]): ∀ (a : exp (list char)) (a_1 : ty) (a_2 a_3 : list char), % 44.91/45.09 Or (Eq (wTrt p h_a e a a_1) False) (Eq (wTrt p h_a e (fAss (list char) e_a a_2 a_3 a) void) True) % 44.91/45.09 Clause #784 (by superposition #[782, 1]): ∀ (a a_1 : list char), Or (Eq (wTrt p h_a e (fAss (list char) e_a a a_1 e_2) void) True) (Eq False True) % 44.91/45.09 Clause #791 (by clausification #[784]): ∀ (a a_1 : list char), Eq (wTrt p h_a e (fAss (list char) e_a a a_1 e_2) void) True % 44.91/45.09 Clause #1571 (by clausification #[98]): Eq % 44.91/45.09 (Exists fun T => % 44.91/45.09 And (wTrt p h_a e (fAss (list char) e_a f d e_2) T) % 44.91/45.09 (widen (product_prod (list (list char)) (exp (list char))) p T t)) % 44.91/45.09 False % 44.91/45.09 Clause #1572 (by clausification #[1571]): ∀ (a : ty), % 44.91/45.09 Eq % 44.91/45.09 (And (wTrt p h_a e (fAss (list char) e_a f d e_2) a) % 44.91/45.09 (widen (product_prod (list (list char)) (exp (list char))) p a t)) % 44.91/45.09 False % 44.91/45.09 Clause #1573 (by clausification #[1572]): ∀ (a : ty), % 44.91/45.09 Or (Eq (wTrt p h_a e (fAss (list char) e_a f d e_2) a) False) % 44.91/45.09 (Eq (widen (product_prod (list (list char)) (exp (list char))) p a t) False) % 44.91/45.09 Clause #1574 (by forward demodulation #[1573, 102]): ∀ (a : ty), % 44.91/45.09 Or (Eq (wTrt p h_a e (fAss (list char) e_a f d e_2) a) False) % 44.91/45.09 (Eq (widen (product_prod (list (list char)) (exp (list char))) p a void) False) % 44.91/45.09 Clause #1575 (by superposition #[1574, 791]): Or (Eq (widen (product_prod (list (list char)) (exp (list char))) p void void) False) (Eq False True) % 44.91/45.09 Clause #1576 (by clausification #[1575]): Eq (widen (product_prod (list (list char)) (exp (list char))) p void void) False % 44.91/45.09 Clause #1577 (by superposition #[1576, 107]): Eq False True % 44.91/45.09 Clause #1578 (by clausification #[1577]): False % 44.91/45.09 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------