%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW562_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n026.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 30.18s 30.37s % Output : Proof 30.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SWW562_5 : TPTP v9.2.0. Released v6.0.0. % 0.04/0.13 % Command : duper %s % 0.13/0.34 % Computer : n026.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:12:38 EDT 2025 % 0.13/0.35 % CPUTime : % 30.18/30.37 SZS status Theorem for theBenchmark.p % 30.18/30.37 SZS output start Proof for theBenchmark.p % 30.18/30.37 Clause #0 (by assumption #[]): Eq % 30.18/30.37 (wt p % 30.18/30.37 (map_upds (list char) ty (combk (option ty) (list char) (none ty)) (cons (list char) this pns) % 30.18/30.37 (cons ty (class d) ts)) % 30.18/30.37 body t) % 30.18/30.37 True % 30.18/30.37 Clause #19 (by assumption #[]): Eq % 30.18/30.37 (∀ (Hb : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))) % 30.18/30.37 (Ta : ty) (Ea : exp (list char)) (Ea1 : fun (list char) (option ty)) % 30.18/30.37 (Pa : % 30.18/30.37 list % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list (product_prod (list char) ty)) % 30.18/30.37 (list % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 30.18/30.37 wt Pa Ea1 Ea Ta → wTrt Pa Hb Ea1 Ea Ta) % 30.18/30.37 True % 30.18/30.37 Clause #107 (by assumption #[]): Eq % 30.18/30.37 (Not % 30.18/30.37 (wTrt p ha % 30.18/30.37 (map_upds (list char) ty (combk (option ty) (list char) (none ty)) (cons (list char) this pns) % 30.18/30.37 (cons ty (class d) ts)) % 30.18/30.37 body t)) % 30.18/30.37 True % 30.18/30.37 Clause #165 (by clausification #[19]): ∀ (a : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 30.18/30.37 Eq % 30.18/30.37 (∀ (Ta : ty) (Ea : exp (list char)) (Ea1 : fun (list char) (option ty)) % 30.18/30.37 (Pa : % 30.18/30.37 list % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list (product_prod (list char) ty)) % 30.18/30.37 (list % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list ty) % 30.18/30.37 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 30.18/30.37 wt Pa Ea1 Ea Ta → wTrt Pa a Ea1 Ea Ta) % 30.18/30.37 True % 30.18/30.37 Clause #166 (by clausification #[165]): ∀ (a : ty) % 30.18/30.37 (a_1 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 30.18/30.37 Eq % 30.18/30.37 (∀ (Ea : exp (list char)) (Ea1 : fun (list char) (option ty)) % 30.18/30.37 (Pa : % 30.18/30.37 list % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list (product_prod (list char) ty)) % 30.18/30.37 (list % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list ty) % 30.18/30.37 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 30.18/30.37 wt Pa Ea1 Ea a → wTrt Pa a_1 Ea1 Ea a) % 30.18/30.37 True % 30.18/30.37 Clause #167 (by clausification #[166]): ∀ (a : exp (list char)) (a_1 : ty) % 30.18/30.37 (a_2 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 30.18/30.37 Eq % 30.18/30.37 (∀ (Ea1 : fun (list char) (option ty)) % 30.18/30.37 (Pa : % 30.18/30.37 list % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list (product_prod (list char) ty)) % 30.18/30.37 (list % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list ty) % 30.18/30.37 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 30.18/30.37 wt Pa Ea1 a a_1 → wTrt Pa a_2 Ea1 a a_1) % 30.18/30.37 True % 30.18/30.37 Clause #168 (by clausification #[167]): ∀ (a : fun (list char) (option ty)) (a_1 : exp (list char)) (a_2 : ty) % 30.18/30.37 (a_3 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 30.18/30.37 Eq % 30.18/30.37 (∀ % 30.18/30.37 (Pa : % 30.18/30.37 list % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list (product_prod (list char) ty)) % 30.18/30.37 (list % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list ty) % 30.18/30.37 (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))), % 30.18/30.37 wt Pa a a_1 a_2 → wTrt Pa a_3 a a_1 a_2) % 30.18/30.37 True % 30.18/30.37 Clause #169 (by clausification #[168]): ∀ % 30.18/30.37 (a : % 30.18/30.37 list % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list (product_prod (list char) ty)) % 30.18/30.37 (list % 30.18/30.37 (product_prod (list char) % 30.18/30.37 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))) % 30.22/30.40 (a_1 : fun (list char) (option ty)) (a_2 : exp (list char)) (a_3 : ty) % 30.22/30.40 (a_4 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 30.22/30.40 Eq (wt a a_1 a_2 a_3 → wTrt a a_4 a_1 a_2 a_3) True % 30.22/30.40 Clause #170 (by clausification #[169]): ∀ % 30.22/30.40 (a : % 30.22/30.40 list % 30.22/30.40 (product_prod (list char) % 30.22/30.40 (product_prod (list char) % 30.22/30.40 (product_prod (list (product_prod (list char) ty)) % 30.22/30.40 (list % 30.22/30.40 (product_prod (list char) % 30.22/30.40 (product_prod (list ty) (product_prod ty (product_prod (list (list char)) (exp (list char))))))))))) % 30.22/30.40 (a_1 : fun (list char) (option ty)) (a_2 : exp (list char)) (a_3 : ty) % 30.22/30.40 (a_4 : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 30.22/30.40 Or (Eq (wt a a_1 a_2 a_3) False) (Eq (wTrt a a_4 a_1 a_2 a_3) True) % 30.22/30.40 Clause #171 (by superposition #[170, 0]): ∀ (a : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 30.22/30.40 Or % 30.22/30.40 (Eq % 30.22/30.40 (wTrt p a % 30.22/30.40 (map_upds (list char) ty (combk (option ty) (list char) (none ty)) (cons (list char) this pns) % 30.22/30.40 (cons ty (class d) ts)) % 30.22/30.40 body t) % 30.22/30.40 True) % 30.22/30.40 (Eq False True) % 30.22/30.40 Clause #3128 (by clausification #[107]): Eq % 30.22/30.40 (wTrt p ha % 30.22/30.40 (map_upds (list char) ty (combk (option ty) (list char) (none ty)) (cons (list char) this pns) % 30.22/30.40 (cons ty (class d) ts)) % 30.22/30.40 body t) % 30.22/30.40 False % 30.22/30.40 Clause #3255 (by clausification #[171]): ∀ (a : fun nat (option (product_prod (list char) (fun (product_prod (list char) (list char)) (option val))))), % 30.22/30.40 Eq % 30.22/30.40 (wTrt p a % 30.22/30.40 (map_upds (list char) ty (combk (option ty) (list char) (none ty)) (cons (list char) this pns) % 30.22/30.40 (cons ty (class d) ts)) % 30.22/30.40 body t) % 30.22/30.40 True % 30.22/30.40 Clause #3256 (by superposition #[3255, 3128]): Eq True False % 30.22/30.40 Clause #3259 (by clausification #[3256]): False % 30.22/30.40 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------