%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP018^3 : TPTP v9.2.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n023.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 3.90s 4.05s % Output : Proof 3.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ITP018^3 : TPTP v9.2.0. Bugfixed v7.5.0. % 0.13/0.14 % Command : duper %s % 0.13/0.35 % Computer : n023.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Oct 2 23:15:38 EDT 2025 % 0.13/0.35 % CPUTime : % 3.90/4.05 SZS status Theorem for theBenchmark.p % 3.90/4.05 SZS output start Proof for theBenchmark.p % 3.90/4.05 Clause #7 (by assumption #[]): Eq % 3.90/4.05 (∀ (A_27a A_27b : Type) (V0x : tyop_2Ebinary__ieee_2Efloat A_27a A_27b), % 3.90/4.05 Eq (c_2Ebinary__ieee_2Efloat__to__real A_27a A_27b (c_2Ebinary__ieee_2Efloat__negate A_27a A_27b V0x)) % 3.90/4.05 (c_2Erealax_2Ereal__neg (c_2Ebinary__ieee_2Efloat__to__real A_27a A_27b V0x))) % 3.90/4.05 True % 3.90/4.05 Clause #8 (by assumption #[]): Eq % 3.90/4.05 (∀ (A_27t A_27w : Type), % 3.90/4.05 Eq (c_2Ebinary__ieee_2Eulp A_27t A_27w (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod A_27t A_27w))) % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__to__real A_27t A_27w % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__plus__min A_27t A_27w (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod A_27t A_27w))))) % 3.90/4.05 True % 3.90/4.05 Clause #11 (by assumption #[]): Eq % 3.90/4.05 (Not % 3.90/4.05 (∀ (A_27t A_27w : Type), % 3.90/4.05 Eq % 3.90/4.05 (c_2Erealax_2Ereal__neg % 3.90/4.05 (c_2Ebinary__ieee_2Eulp A_27t A_27w (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod A_27t A_27w)))) % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__to__real A_27t A_27w % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__negate A_27t A_27w % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__plus__min A_27t A_27w % 3.90/4.05 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod A_27t A_27w))))))) % 3.90/4.05 True % 3.90/4.05 Clause #199 (by clausification #[7]): ∀ (a : Type), % 3.90/4.05 Eq % 3.90/4.05 (∀ (A_27b : Type) (V0x : tyop_2Ebinary__ieee_2Efloat a A_27b), % 3.90/4.05 Eq (c_2Ebinary__ieee_2Efloat__to__real a A_27b (c_2Ebinary__ieee_2Efloat__negate a A_27b V0x)) % 3.90/4.05 (c_2Erealax_2Ereal__neg (c_2Ebinary__ieee_2Efloat__to__real a A_27b V0x))) % 3.90/4.05 True % 3.90/4.05 Clause #200 (by clausification #[199]): ∀ (a a_1 : Type), % 3.90/4.05 Eq % 3.90/4.05 (∀ (V0x : tyop_2Ebinary__ieee_2Efloat a a_1), % 3.90/4.05 Eq (c_2Ebinary__ieee_2Efloat__to__real a a_1 (c_2Ebinary__ieee_2Efloat__negate a a_1 V0x)) % 3.90/4.05 (c_2Erealax_2Ereal__neg (c_2Ebinary__ieee_2Efloat__to__real a a_1 V0x))) % 3.90/4.05 True % 3.90/4.05 Clause #201 (by clausification #[200]): ∀ (a a_1 : Type) (a_2 : tyop_2Ebinary__ieee_2Efloat a a_1), % 3.90/4.05 Eq % 3.90/4.05 (Eq (c_2Ebinary__ieee_2Efloat__to__real a a_1 (c_2Ebinary__ieee_2Efloat__negate a a_1 a_2)) % 3.90/4.05 (c_2Erealax_2Ereal__neg (c_2Ebinary__ieee_2Efloat__to__real a a_1 a_2))) % 3.90/4.05 True % 3.90/4.05 Clause #202 (by clausification #[201]): ∀ (a a_1 : Type) (a_2 : tyop_2Ebinary__ieee_2Efloat a a_1), % 3.90/4.05 Eq (c_2Ebinary__ieee_2Efloat__to__real a a_1 (c_2Ebinary__ieee_2Efloat__negate a a_1 a_2)) % 3.90/4.05 (c_2Erealax_2Ereal__neg (c_2Ebinary__ieee_2Efloat__to__real a a_1 a_2)) % 3.90/4.05 Clause #286 (by clausification #[8]): ∀ (a : Type), % 3.90/4.05 Eq % 3.90/4.05 (∀ (A_27w : Type), % 3.90/4.05 Eq (c_2Ebinary__ieee_2Eulp a A_27w (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod a A_27w))) % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__to__real a A_27w % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__plus__min a A_27w (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod a A_27w))))) % 3.90/4.05 True % 3.90/4.05 Clause #287 (by clausification #[286]): ∀ (a a_1 : Type), % 3.90/4.05 Eq % 3.90/4.05 (Eq (c_2Ebinary__ieee_2Eulp a a_1 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod a a_1))) % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__to__real a a_1 % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__plus__min a a_1 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod a a_1))))) % 3.90/4.05 True % 3.90/4.05 Clause #288 (by clausification #[287]): ∀ (a a_1 : Type), % 3.90/4.05 Eq (c_2Ebinary__ieee_2Eulp a a_1 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod a a_1))) % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__to__real a a_1 % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__plus__min a a_1 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod a a_1)))) % 3.90/4.05 Clause #345 (by clausification #[11]): Eq % 3.90/4.05 (∀ (A_27t A_27w : Type), % 3.90/4.05 Eq % 3.90/4.05 (c_2Erealax_2Ereal__neg % 3.90/4.05 (c_2Ebinary__ieee_2Eulp A_27t A_27w (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod A_27t A_27w)))) % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__to__real A_27t A_27w % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__negate A_27t A_27w % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__plus__min A_27t A_27w (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod A_27t A_27w)))))) % 3.90/4.05 False % 3.90/4.05 Clause #346 (by clausification #[345]): ∀ (a : Type), % 3.90/4.05 Eq % 3.90/4.05 (Not % 3.90/4.05 (∀ (A_27w : Type), % 3.90/4.05 Eq % 3.90/4.05 (c_2Erealax_2Ereal__neg % 3.90/4.05 (c_2Ebinary__ieee_2Eulp (skS.0 2 a) A_27w (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)))) % 3.90/4.05 (c_2Ebinary__ieee_2Efloat__to__real (skS.0 2 a) A_27w % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__negate (skS.0 2 a) A_27w % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__plus__min (skS.0 2 a) A_27w % 3.90/4.07 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) A_27w))))))) % 3.90/4.07 True % 3.90/4.07 Clause #347 (by clausification #[346]): ∀ (a : Type), % 3.90/4.07 Eq % 3.90/4.07 (∀ (A_27w : Type), % 3.90/4.07 Eq % 3.90/4.07 (c_2Erealax_2Ereal__neg % 3.90/4.07 (c_2Ebinary__ieee_2Eulp (skS.0 2 a) A_27w (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)))) % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__to__real (skS.0 2 a) A_27w % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__negate (skS.0 2 a) A_27w % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__plus__min (skS.0 2 a) A_27w % 3.90/4.07 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)))))) % 3.90/4.07 False % 3.90/4.07 Clause #348 (by clausification #[347]): ∀ (a a_1 : Type), % 3.90/4.07 Eq % 3.90/4.07 (Not % 3.90/4.07 (Eq % 3.90/4.07 (c_2Erealax_2Ereal__neg % 3.90/4.07 (c_2Ebinary__ieee_2Eulp (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))) % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__to__real (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__negate (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__plus__min (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1)))))))) % 3.90/4.07 True % 3.90/4.07 Clause #349 (by clausification #[348]): ∀ (a a_1 : Type), % 3.90/4.07 Eq % 3.90/4.07 (Eq % 3.90/4.07 (c_2Erealax_2Ereal__neg % 3.90/4.07 (c_2Ebinary__ieee_2Eulp (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))) % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__to__real (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__negate (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__plus__min (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))))) % 3.90/4.07 False % 3.90/4.07 Clause #350 (by clausification #[349]): ∀ (a a_1 : Type), % 3.90/4.07 Ne % 3.90/4.07 (c_2Erealax_2Ereal__neg % 3.90/4.07 (c_2Ebinary__ieee_2Eulp (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))) % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__to__real (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__negate (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__plus__min (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1)))))) % 3.90/4.07 Clause #351 (by forward demodulation #[350, 202]): ∀ (a a_1 : Type), % 3.90/4.07 Ne % 3.90/4.07 (c_2Erealax_2Ereal__neg % 3.90/4.07 (c_2Ebinary__ieee_2Eulp (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))) % 3.90/4.07 (c_2Erealax_2Ereal__neg % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__to__real (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebinary__ieee_2Efloat__plus__min (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1)))))) % 3.90/4.07 Clause #352 (by forward demodulation #[351, 288]): ∀ (a a_1 : Type), % 3.90/4.07 Ne % 3.90/4.07 (c_2Erealax_2Ereal__neg % 3.90/4.07 (c_2Ebinary__ieee_2Eulp (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))) % 3.90/4.07 (c_2Erealax_2Ereal__neg % 3.90/4.07 (c_2Ebinary__ieee_2Eulp (skS.0 2 a) (skS.0 3 a a_1) % 3.90/4.07 (c_2Ebool_2Ethe__value (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))))) % 3.90/4.07 Clause #353 (by eliminate resolved literals #[352]): False % 3.90/4.07 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------