%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP018+1 : TPTP v9.2.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n011.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 07:50:56 PM UTC 2025 % Result : Theorem 6.18s 6.37s % Output : Proof 6.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : ITP018+1 : TPTP v9.2.0. Bugfixed v7.5.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n011.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 22:33:23 EDT 2025 % 0.13/0.35 % CPUTime : % 6.18/6.37 SZS status Theorem for theBenchmark.p % 6.18/6.37 SZS output start Proof for theBenchmark.p % 6.18/6.37 Clause #27 (by assumption #[]): Eq % 6.18/6.37 (∀ (A_27a A_27b V0x_2E0 : Iota), % 6.18/6.37 Eq % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.37 (s (tyop_2Ebinary__ieee_2Efloat A_27a A_27b) % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__negate_2E1 (s (tyop_2Ebinary__ieee_2Efloat A_27a A_27b) V0x_2E0))))) % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (s (tyop_2Ebinary__ieee_2Efloat A_27a A_27b) V0x_2E0)))))) % 6.18/6.37 True % 6.18/6.37 Clause #28 (by assumption #[]): Eq % 6.18/6.37 (∀ (A_27t A_27w : Iota), % 6.18/6.37 Eq % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Eulp_2E1 % 6.18/6.37 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod A_27t A_27w)) c_2Ebool_2Ethe__value_2E0))) % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.37 (s (tyop_2Ebinary__ieee_2Efloat A_27t A_27w) % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.18/6.37 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod A_27t A_27w)) c_2Ebool_2Ethe__value_2E0)))))) % 6.18/6.37 True % 6.18/6.37 Clause #30 (by assumption #[]): Eq % 6.18/6.37 (Not % 6.18/6.37 (∀ (A_27t A_27w : Iota), % 6.18/6.37 Eq % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Eulp_2E1 % 6.18/6.37 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod A_27t A_27w)) c_2Ebool_2Ethe__value_2E0))))) % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.37 (s (tyop_2Ebinary__ieee_2Efloat A_27t A_27w) % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.18/6.37 (s (tyop_2Ebinary__ieee_2Efloat A_27t A_27w) % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.18/6.37 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod A_27t A_27w)) c_2Ebool_2Ethe__value_2E0))))))))) % 6.18/6.37 True % 6.18/6.37 Clause #1180 (by clausification #[27]): ∀ (a : Iota), % 6.18/6.37 Eq % 6.18/6.37 (∀ (A_27b V0x_2E0 : Iota), % 6.18/6.37 Eq % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.37 (s (tyop_2Ebinary__ieee_2Efloat a A_27b) % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__negate_2E1 (s (tyop_2Ebinary__ieee_2Efloat a A_27b) V0x_2E0))))) % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (s (tyop_2Ebinary__ieee_2Efloat a A_27b) V0x_2E0)))))) % 6.18/6.37 True % 6.18/6.37 Clause #1181 (by clausification #[1180]): ∀ (a a_1 : Iota), % 6.18/6.37 Eq % 6.18/6.37 (∀ (V0x_2E0 : Iota), % 6.18/6.37 Eq % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.37 (s (tyop_2Ebinary__ieee_2Efloat a a_1) % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__negate_2E1 (s (tyop_2Ebinary__ieee_2Efloat a a_1) V0x_2E0))))) % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (s (tyop_2Ebinary__ieee_2Efloat a a_1) V0x_2E0)))))) % 6.18/6.37 True % 6.18/6.37 Clause #1182 (by clausification #[1181]): ∀ (a a_1 a_2 : Iota), % 6.18/6.37 Eq % 6.18/6.37 (Eq % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.37 (s (tyop_2Ebinary__ieee_2Efloat a a_1) % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__negate_2E1 (s (tyop_2Ebinary__ieee_2Efloat a a_1) a_2))))) % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (s (tyop_2Ebinary__ieee_2Efloat a a_1) a_2)))))) % 6.18/6.37 True % 6.18/6.37 Clause #1183 (by clausification #[1182]): ∀ (a a_1 a_2 : Iota), % 6.18/6.37 Eq % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.37 (s (tyop_2Ebinary__ieee_2Efloat a a_1) % 6.18/6.37 (c_2Ebinary__ieee_2Efloat__negate_2E1 (s (tyop_2Ebinary__ieee_2Efloat a a_1) a_2))))) % 6.18/6.37 (s tyop_2Erealax_2Ereal % 6.18/6.37 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.37 (s tyop_2Erealax_2Ereal (c_2Ebinary__ieee_2Efloat__to__real_2E1 (s (tyop_2Ebinary__ieee_2Efloat a a_1) a_2))))) % 6.18/6.37 Clause #1201 (by clausification #[28]): ∀ (a : Iota), % 6.18/6.37 Eq % 6.18/6.37 (∀ (A_27w : Iota), % 6.18/6.38 Eq % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Ebinary__ieee_2Eulp_2E1 % 6.18/6.38 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod a A_27w)) c_2Ebool_2Ethe__value_2E0))) % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.38 (s (tyop_2Ebinary__ieee_2Efloat a A_27w) % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.18/6.38 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod a A_27w)) c_2Ebool_2Ethe__value_2E0)))))) % 6.18/6.38 True % 6.18/6.38 Clause #1202 (by clausification #[1201]): ∀ (a a_1 : Iota), % 6.18/6.38 Eq % 6.18/6.38 (Eq % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Ebinary__ieee_2Eulp_2E1 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod a a_1)) c_2Ebool_2Ethe__value_2E0))) % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.38 (s (tyop_2Ebinary__ieee_2Efloat a a_1) % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.18/6.38 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod a a_1)) c_2Ebool_2Ethe__value_2E0)))))) % 6.18/6.38 True % 6.18/6.38 Clause #1203 (by clausification #[1202]): ∀ (a a_1 : Iota), % 6.18/6.38 Eq % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Ebinary__ieee_2Eulp_2E1 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod a a_1)) c_2Ebool_2Ethe__value_2E0))) % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.38 (s (tyop_2Ebinary__ieee_2Efloat a a_1) % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.18/6.38 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod a a_1)) c_2Ebool_2Ethe__value_2E0))))) % 6.18/6.38 Clause #1217 (by clausification #[30]): Eq % 6.18/6.38 (∀ (A_27t A_27w : Iota), % 6.18/6.38 Eq % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Ebinary__ieee_2Eulp_2E1 % 6.18/6.38 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod A_27t A_27w)) c_2Ebool_2Ethe__value_2E0))))) % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.38 (s (tyop_2Ebinary__ieee_2Efloat A_27t A_27w) % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.18/6.38 (s (tyop_2Ebinary__ieee_2Efloat A_27t A_27w) % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.18/6.38 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod A_27t A_27w)) c_2Ebool_2Ethe__value_2E0)))))))) % 6.18/6.38 False % 6.18/6.38 Clause #1218 (by clausification #[1217]): ∀ (a : Iota), % 6.18/6.38 Eq % 6.18/6.38 (Not % 6.18/6.38 (∀ (A_27w : Iota), % 6.18/6.38 Eq % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Ebinary__ieee_2Eulp_2E1 % 6.18/6.38 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)) c_2Ebool_2Ethe__value_2E0))))) % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.38 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) A_27w) % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.18/6.38 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) A_27w) % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.18/6.38 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)) % 6.18/6.38 c_2Ebool_2Ethe__value_2E0))))))))) % 6.18/6.38 True % 6.18/6.38 Clause #1219 (by clausification #[1218]): ∀ (a : Iota), % 6.18/6.38 Eq % 6.18/6.38 (∀ (A_27w : Iota), % 6.18/6.38 Eq % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Ebinary__ieee_2Eulp_2E1 % 6.18/6.38 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)) c_2Ebool_2Ethe__value_2E0))))) % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.38 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) A_27w) % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.18/6.38 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) A_27w) % 6.18/6.38 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.18/6.38 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)) c_2Ebool_2Ethe__value_2E0)))))))) % 6.18/6.38 False % 6.18/6.38 Clause #1220 (by clausification #[1219]): ∀ (a a_1 : Iota), % 6.18/6.38 Eq % 6.18/6.38 (Not % 6.18/6.38 (Eq % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.38 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.38 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Ebinary__ieee_2Eulp_2E1 % 6.18/6.40 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) % 6.18/6.40 c_2Ebool_2Ethe__value_2E0))))) % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.40 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.18/6.40 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.18/6.40 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.18/6.40 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.18/6.40 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) % 6.18/6.40 c_2Ebool_2Ethe__value_2E0))))))))) % 6.18/6.40 True % 6.18/6.40 Clause #1221 (by clausification #[1220]): ∀ (a a_1 : Iota), % 6.18/6.40 Eq % 6.18/6.40 (Eq % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Ebinary__ieee_2Eulp_2E1 % 6.18/6.40 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) c_2Ebool_2Ethe__value_2E0))))) % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.40 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.18/6.40 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.18/6.40 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.18/6.40 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.18/6.40 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) % 6.18/6.40 c_2Ebool_2Ethe__value_2E0)))))))) % 6.18/6.40 False % 6.18/6.40 Clause #1222 (by clausification #[1221]): ∀ (a a_1 : Iota), % 6.18/6.40 Ne % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Ebinary__ieee_2Eulp_2E1 % 6.18/6.40 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) c_2Ebool_2Ethe__value_2E0))))) % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.40 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.18/6.40 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.18/6.40 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.18/6.40 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.18/6.40 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) % 6.18/6.40 c_2Ebool_2Ethe__value_2E0))))))) % 6.18/6.40 Clause #1223 (by forward demodulation #[1222, 1183]): ∀ (a a_1 : Iota), % 6.18/6.40 Ne % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Ebinary__ieee_2Eulp_2E1 % 6.18/6.40 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) c_2Ebool_2Ethe__value_2E0))))) % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.18/6.40 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.18/6.40 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.18/6.40 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) % 6.18/6.40 c_2Ebool_2Ethe__value_2E0))))))) % 6.18/6.40 Clause #1224 (by forward demodulation #[1223, 1203]): ∀ (a a_1 : Iota), % 6.18/6.40 Ne % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Ebinary__ieee_2Eulp_2E1 % 6.18/6.40 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) c_2Ebool_2Ethe__value_2E0))))) % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Erealax_2Ereal__neg_2E1 % 6.18/6.40 (s tyop_2Erealax_2Ereal % 6.18/6.40 (c_2Ebinary__ieee_2Eulp_2E1 % 6.18/6.40 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) c_2Ebool_2Ethe__value_2E0))))) % 6.18/6.40 Clause #1225 (by eliminate resolved literals #[1224]): False % 6.18/6.40 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------