%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP018_3 : TPTP v9.2.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n027.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 4.52s 4.69s % Output : Proof 4.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : ITP018_3 : TPTP v9.2.0. Bugfixed v7.5.0. % 0.07/0.14 % Command : duper %s % 0.14/0.35 % Computer : n027.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.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Thu Oct 2 22:45:38 EDT 2025 % 0.14/0.36 % CPUTime : % 4.52/4.69 SZS status Theorem for theBenchmark.p % 4.52/4.69 SZS output start Proof for theBenchmark.p % 4.52/4.69 Clause #27 (by assumption #[]): Eq % 4.52/4.69 (∀ (A_27a A_27b : Type) (V0x_2E0 : tyop_2Ebinary__ieee_2Efloat A_27a A_27b), % 4.52/4.69 Eq (c_2Ebinary__ieee_2Efloat__to__real_2E1 A_27a A_27b (c_2Ebinary__ieee_2Efloat__negate_2E1 A_27a A_27b V0x_2E0)) % 4.52/4.69 (c_2Erealax_2Ereal__neg_2E1 (c_2Ebinary__ieee_2Efloat__to__real_2E1 A_27a A_27b V0x_2E0))) % 4.52/4.69 True % 4.52/4.69 Clause #28 (by assumption #[]): Eq % 4.52/4.69 (∀ (A_27t A_27w : Type), % 4.52/4.69 Eq (c_2Ebinary__ieee_2Eulp_2E1 A_27t A_27w (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod A_27t A_27w))) % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__to__real_2E1 A_27t A_27w % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 A_27t A_27w % 4.52/4.69 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod A_27t A_27w))))) % 4.52/4.69 True % 4.52/4.69 Clause #30 (by assumption #[]): Eq % 4.52/4.69 (Not % 4.52/4.69 (∀ (A_27t A_27w : Type), % 4.52/4.69 Eq % 4.52/4.69 (c_2Erealax_2Ereal__neg_2E1 % 4.52/4.69 (c_2Ebinary__ieee_2Eulp_2E1 A_27t A_27w (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod A_27t A_27w)))) % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__to__real_2E1 A_27t A_27w % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__negate_2E1 A_27t A_27w % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 A_27t A_27w % 4.52/4.69 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod A_27t A_27w))))))) % 4.52/4.69 True % 4.52/4.69 Clause #912 (by clausification #[27]): ∀ (a : Type), % 4.52/4.69 Eq % 4.52/4.69 (∀ (A_27b : Type) (V0x_2E0 : tyop_2Ebinary__ieee_2Efloat a A_27b), % 4.52/4.69 Eq (c_2Ebinary__ieee_2Efloat__to__real_2E1 a A_27b (c_2Ebinary__ieee_2Efloat__negate_2E1 a A_27b V0x_2E0)) % 4.52/4.69 (c_2Erealax_2Ereal__neg_2E1 (c_2Ebinary__ieee_2Efloat__to__real_2E1 a A_27b V0x_2E0))) % 4.52/4.69 True % 4.52/4.69 Clause #913 (by clausification #[912]): ∀ (a a_1 : Type), % 4.52/4.69 Eq % 4.52/4.69 (∀ (V0x_2E0 : tyop_2Ebinary__ieee_2Efloat a a_1), % 4.52/4.69 Eq (c_2Ebinary__ieee_2Efloat__to__real_2E1 a a_1 (c_2Ebinary__ieee_2Efloat__negate_2E1 a a_1 V0x_2E0)) % 4.52/4.69 (c_2Erealax_2Ereal__neg_2E1 (c_2Ebinary__ieee_2Efloat__to__real_2E1 a a_1 V0x_2E0))) % 4.52/4.69 True % 4.52/4.69 Clause #914 (by clausification #[913]): ∀ (a a_1 : Type) (a_2 : tyop_2Ebinary__ieee_2Efloat a a_1), % 4.52/4.69 Eq % 4.52/4.69 (Eq (c_2Ebinary__ieee_2Efloat__to__real_2E1 a a_1 (c_2Ebinary__ieee_2Efloat__negate_2E1 a a_1 a_2)) % 4.52/4.69 (c_2Erealax_2Ereal__neg_2E1 (c_2Ebinary__ieee_2Efloat__to__real_2E1 a a_1 a_2))) % 4.52/4.69 True % 4.52/4.69 Clause #915 (by clausification #[914]): ∀ (a a_1 : Type) (a_2 : tyop_2Ebinary__ieee_2Efloat a a_1), % 4.52/4.69 Eq (c_2Ebinary__ieee_2Efloat__to__real_2E1 a a_1 (c_2Ebinary__ieee_2Efloat__negate_2E1 a a_1 a_2)) % 4.52/4.69 (c_2Erealax_2Ereal__neg_2E1 (c_2Ebinary__ieee_2Efloat__to__real_2E1 a a_1 a_2)) % 4.52/4.69 Clause #918 (by clausification #[28]): ∀ (a : Type), % 4.52/4.69 Eq % 4.52/4.69 (∀ (A_27w : Type), % 4.52/4.69 Eq (c_2Ebinary__ieee_2Eulp_2E1 a A_27w (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod a A_27w))) % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__to__real_2E1 a A_27w % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 a A_27w (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod a A_27w))))) % 4.52/4.69 True % 4.52/4.69 Clause #919 (by clausification #[918]): ∀ (a a_1 : Type), % 4.52/4.69 Eq % 4.52/4.69 (Eq (c_2Ebinary__ieee_2Eulp_2E1 a a_1 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod a a_1))) % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__to__real_2E1 a a_1 % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 a a_1 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod a a_1))))) % 4.52/4.69 True % 4.52/4.69 Clause #920 (by clausification #[919]): ∀ (a a_1 : Type), % 4.52/4.69 Eq (c_2Ebinary__ieee_2Eulp_2E1 a a_1 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod a a_1))) % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__to__real_2E1 a a_1 % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 a a_1 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod a a_1)))) % 4.52/4.69 Clause #1165 (by clausification #[30]): Eq % 4.52/4.69 (∀ (A_27t A_27w : Type), % 4.52/4.69 Eq % 4.52/4.69 (c_2Erealax_2Ereal__neg_2E1 % 4.52/4.69 (c_2Ebinary__ieee_2Eulp_2E1 A_27t A_27w (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod A_27t A_27w)))) % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__to__real_2E1 A_27t A_27w % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__negate_2E1 A_27t A_27w % 4.52/4.69 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 A_27t A_27w % 4.52/4.69 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod A_27t A_27w)))))) % 4.52/4.69 False % 4.52/4.69 Clause #1166 (by clausification #[1165]): ∀ (a : Type), % 4.52/4.70 Eq % 4.52/4.70 (Not % 4.52/4.70 (∀ (A_27w : Type), % 4.52/4.70 Eq % 4.52/4.70 (c_2Erealax_2Ereal__neg_2E1 % 4.52/4.70 (c_2Ebinary__ieee_2Eulp_2E1 (skS.0 2 a) A_27w % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)))) % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (skS.0 2 a) A_27w % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__negate_2E1 (skS.0 2 a) A_27w % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 (skS.0 2 a) A_27w % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) A_27w))))))) % 4.52/4.70 True % 4.52/4.70 Clause #1167 (by clausification #[1166]): ∀ (a : Type), % 4.52/4.70 Eq % 4.52/4.70 (∀ (A_27w : Type), % 4.52/4.70 Eq % 4.52/4.70 (c_2Erealax_2Ereal__neg_2E1 % 4.52/4.70 (c_2Ebinary__ieee_2Eulp_2E1 (skS.0 2 a) A_27w % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)))) % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (skS.0 2 a) A_27w % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__negate_2E1 (skS.0 2 a) A_27w % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 (skS.0 2 a) A_27w % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)))))) % 4.52/4.70 False % 4.52/4.70 Clause #1168 (by clausification #[1167]): ∀ (a a_1 : Type), % 4.52/4.70 Eq % 4.52/4.70 (Not % 4.52/4.70 (Eq % 4.52/4.70 (c_2Erealax_2Ereal__neg_2E1 % 4.52/4.70 (c_2Ebinary__ieee_2Eulp_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))) % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__negate_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1)))))))) % 4.52/4.70 True % 4.52/4.70 Clause #1169 (by clausification #[1168]): ∀ (a a_1 : Type), % 4.52/4.70 Eq % 4.52/4.70 (Eq % 4.52/4.70 (c_2Erealax_2Ereal__neg_2E1 % 4.52/4.70 (c_2Ebinary__ieee_2Eulp_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))) % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__negate_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))))) % 4.52/4.70 False % 4.52/4.70 Clause #1170 (by clausification #[1169]): ∀ (a a_1 : Type), % 4.52/4.70 Ne % 4.52/4.70 (c_2Erealax_2Ereal__neg_2E1 % 4.52/4.70 (c_2Ebinary__ieee_2Eulp_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))) % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__negate_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1)))))) % 4.52/4.70 Clause #1171 (by forward demodulation #[1170, 915]): ∀ (a a_1 : Type), % 4.52/4.70 Ne % 4.52/4.70 (c_2Erealax_2Ereal__neg_2E1 % 4.52/4.70 (c_2Ebinary__ieee_2Eulp_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))) % 4.52/4.70 (c_2Erealax_2Ereal__neg_2E1 % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1)))))) % 4.52/4.70 Clause #1172 (by forward demodulation #[1171, 920]): ∀ (a a_1 : Type), % 4.52/4.70 Ne % 4.52/4.70 (c_2Erealax_2Ereal__neg_2E1 % 4.52/4.70 (c_2Ebinary__ieee_2Eulp_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))) % 4.52/4.70 (c_2Erealax_2Ereal__neg_2E1 % 4.52/4.70 (c_2Ebinary__ieee_2Eulp_2E1 (skS.0 2 a) (skS.0 3 a a_1) % 4.52/4.70 (c_2Ebool_2Ethe__value_2E0 (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))) % 4.52/4.70 Clause #1173 (by eliminate resolved literals #[1172]): False % 4.52/4.70 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------