%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP018_1 : TPTP v9.2.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n003.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.25s 6.50s % Output : Proof 6.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : ITP018_1 : TPTP v9.2.0. Bugfixed v7.5.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n003.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 23:40:53 EDT 2025 % 0.13/0.34 % CPUTime : % 6.25/6.50 SZS status Theorem for theBenchmark.p % 6.25/6.50 SZS output start Proof for theBenchmark.p % 6.25/6.50 Clause #40 (by assumption #[]): Eq % 6.25/6.50 (∀ (A_27a A_27b : d) (V0x_2E0 : u), % 6.25/6.50 Eq % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.25/6.50 (s (tyop_2Ebinary__ieee_2Efloat A_27a A_27b) % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__negate_2E1 (s (tyop_2Ebinary__ieee_2Efloat A_27a A_27b) V0x_2E0)))))) % 6.25/6.50 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (s (tyop_2Ebinary__ieee_2Efloat A_27a A_27b) V0x_2E0)))))) % 6.25/6.50 True % 6.25/6.50 Clause #41 (by assumption #[]): Eq % 6.25/6.50 (∀ (A_27t A_27w : d), % 6.25/6.50 Eq % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.25/6.50 (c_2Ebinary__ieee_2Eulp_2E1 % 6.25/6.50 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod A_27t A_27w)) c_2Ebool_2Ethe__value_2E0)))) % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.25/6.50 (s (tyop_2Ebinary__ieee_2Efloat A_27t A_27w) % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.25/6.50 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod A_27t A_27w)) c_2Ebool_2Ethe__value_2E0))))))) % 6.25/6.50 True % 6.25/6.50 Clause #43 (by assumption #[]): Eq % 6.25/6.50 (Not % 6.25/6.50 (∀ (A_27t A_27w : d), % 6.25/6.50 Eq % 6.25/6.50 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.25/6.50 (c_2Ebinary__ieee_2Eulp_2E1 % 6.25/6.50 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod A_27t A_27w)) c_2Ebool_2Ethe__value_2E0))))) % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.25/6.50 (s (tyop_2Ebinary__ieee_2Efloat A_27t A_27w) % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.25/6.50 (s (tyop_2Ebinary__ieee_2Efloat A_27t A_27w) % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.25/6.50 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod A_27t A_27w)) c_2Ebool_2Ethe__value_2E0)))))))))) % 6.25/6.50 True % 6.25/6.50 Clause #1613 (by clausification #[40]): ∀ (a : d), % 6.25/6.50 Eq % 6.25/6.50 (∀ (A_27b : d) (V0x_2E0 : u), % 6.25/6.50 Eq % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.25/6.50 (s (tyop_2Ebinary__ieee_2Efloat a A_27b) % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__negate_2E1 (s (tyop_2Ebinary__ieee_2Efloat a A_27b) V0x_2E0)))))) % 6.25/6.50 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (s (tyop_2Ebinary__ieee_2Efloat a A_27b) V0x_2E0)))))) % 6.25/6.50 True % 6.25/6.50 Clause #1614 (by clausification #[1613]): ∀ (a a_1 : d), % 6.25/6.50 Eq % 6.25/6.50 (∀ (V0x_2E0 : u), % 6.25/6.50 Eq % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.25/6.50 (s (tyop_2Ebinary__ieee_2Efloat a a_1) % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__negate_2E1 (s (tyop_2Ebinary__ieee_2Efloat a a_1) V0x_2E0)))))) % 6.25/6.50 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (s (tyop_2Ebinary__ieee_2Efloat a a_1) V0x_2E0)))))) % 6.25/6.50 True % 6.25/6.50 Clause #1615 (by clausification #[1614]): ∀ (a a_1 : d) (a_2 : u), % 6.25/6.50 Eq % 6.25/6.50 (Eq % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.25/6.50 (s (tyop_2Ebinary__ieee_2Efloat a a_1) % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__negate_2E1 (s (tyop_2Ebinary__ieee_2Efloat a a_1) a_2)))))) % 6.25/6.50 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.25/6.50 (c_2Ebinary__ieee_2Efloat__to__real_2E1 (s (tyop_2Ebinary__ieee_2Efloat a a_1) a_2)))))) % 6.25/6.50 True % 6.25/6.50 Clause #1616 (by clausification #[1615]): ∀ (a a_1 : d) (a_2 : u), % 6.25/6.50 Eq % 6.25/6.50 (j_mono_2Etyop_2Erealax_2Ereal % 6.25/6.50 (s tyop_2Erealax_2Ereal % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.35/6.51 (s (tyop_2Ebinary__ieee_2Efloat a a_1) % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__negate_2E1 (s (tyop_2Ebinary__ieee_2Efloat a a_1) a_2)))))) % 6.35/6.51 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.35/6.51 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.51 (s tyop_2Erealax_2Ereal (c_2Ebinary__ieee_2Efloat__to__real_2E1 (s (tyop_2Ebinary__ieee_2Efloat a a_1) a_2))))) % 6.35/6.51 Clause #1622 (by clausification #[41]): ∀ (a : d), % 6.35/6.51 Eq % 6.35/6.51 (∀ (A_27w : d), % 6.35/6.51 Eq % 6.35/6.51 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.51 (s tyop_2Erealax_2Ereal % 6.35/6.51 (c_2Ebinary__ieee_2Eulp_2E1 % 6.35/6.51 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod a A_27w)) c_2Ebool_2Ethe__value_2E0)))) % 6.35/6.51 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.51 (s tyop_2Erealax_2Ereal % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.35/6.51 (s (tyop_2Ebinary__ieee_2Efloat a A_27w) % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.35/6.51 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod a A_27w)) c_2Ebool_2Ethe__value_2E0))))))) % 6.35/6.51 True % 6.35/6.51 Clause #1623 (by clausification #[1622]): ∀ (a a_1 : d), % 6.35/6.51 Eq % 6.35/6.51 (Eq % 6.35/6.51 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.51 (s tyop_2Erealax_2Ereal % 6.35/6.51 (c_2Ebinary__ieee_2Eulp_2E1 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod a a_1)) c_2Ebool_2Ethe__value_2E0)))) % 6.35/6.51 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.51 (s tyop_2Erealax_2Ereal % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.35/6.51 (s (tyop_2Ebinary__ieee_2Efloat a a_1) % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.35/6.51 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod a a_1)) c_2Ebool_2Ethe__value_2E0))))))) % 6.35/6.51 True % 6.35/6.51 Clause #1624 (by clausification #[1623]): ∀ (a a_1 : d), % 6.35/6.51 Eq % 6.35/6.51 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.51 (s tyop_2Erealax_2Ereal % 6.35/6.51 (c_2Ebinary__ieee_2Eulp_2E1 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod a a_1)) c_2Ebool_2Ethe__value_2E0)))) % 6.35/6.51 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.51 (s tyop_2Erealax_2Ereal % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.35/6.51 (s (tyop_2Ebinary__ieee_2Efloat a a_1) % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.35/6.51 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod a a_1)) c_2Ebool_2Ethe__value_2E0)))))) % 6.35/6.51 Clause #1801 (by clausification #[43]): Eq % 6.35/6.51 (∀ (A_27t A_27w : d), % 6.35/6.51 Eq % 6.35/6.51 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.35/6.51 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.51 (s tyop_2Erealax_2Ereal % 6.35/6.51 (c_2Ebinary__ieee_2Eulp_2E1 % 6.35/6.51 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod A_27t A_27w)) c_2Ebool_2Ethe__value_2E0))))) % 6.35/6.51 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.51 (s tyop_2Erealax_2Ereal % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.35/6.51 (s (tyop_2Ebinary__ieee_2Efloat A_27t A_27w) % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.35/6.51 (s (tyop_2Ebinary__ieee_2Efloat A_27t A_27w) % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.35/6.51 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod A_27t A_27w)) c_2Ebool_2Ethe__value_2E0))))))))) % 6.35/6.51 False % 6.35/6.51 Clause #1802 (by clausification #[1801]): ∀ (a : d), % 6.35/6.51 Eq % 6.35/6.51 (Not % 6.35/6.51 (∀ (A_27w : d), % 6.35/6.51 Eq % 6.35/6.51 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.35/6.51 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.51 (s tyop_2Erealax_2Ereal % 6.35/6.51 (c_2Ebinary__ieee_2Eulp_2E1 % 6.35/6.51 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)) c_2Ebool_2Ethe__value_2E0))))) % 6.35/6.51 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.51 (s tyop_2Erealax_2Ereal % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.35/6.51 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) A_27w) % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.35/6.51 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) A_27w) % 6.35/6.51 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.35/6.51 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)) % 6.35/6.51 c_2Ebool_2Ethe__value_2E0)))))))))) % 6.35/6.51 True % 6.35/6.51 Clause #1803 (by clausification #[1802]): ∀ (a : d), % 6.35/6.51 Eq % 6.35/6.51 (∀ (A_27w : d), % 6.35/6.51 Eq % 6.35/6.51 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.35/6.51 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.52 (s tyop_2Erealax_2Ereal % 6.35/6.52 (c_2Ebinary__ieee_2Eulp_2E1 % 6.35/6.52 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)) c_2Ebool_2Ethe__value_2E0))))) % 6.35/6.52 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.52 (s tyop_2Erealax_2Ereal % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.35/6.52 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) A_27w) % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.35/6.52 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) A_27w) % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.35/6.52 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) A_27w)) % 6.35/6.52 c_2Ebool_2Ethe__value_2E0))))))))) % 6.35/6.52 False % 6.35/6.52 Clause #1804 (by clausification #[1803]): ∀ (a a_1 : d), % 6.35/6.52 Eq % 6.35/6.52 (Not % 6.35/6.52 (Eq % 6.35/6.52 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.35/6.52 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.52 (s tyop_2Erealax_2Ereal % 6.35/6.52 (c_2Ebinary__ieee_2Eulp_2E1 % 6.35/6.52 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) % 6.35/6.52 c_2Ebool_2Ethe__value_2E0))))) % 6.35/6.52 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.52 (s tyop_2Erealax_2Ereal % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.35/6.52 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.35/6.52 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.35/6.52 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) % 6.35/6.52 c_2Ebool_2Ethe__value_2E0)))))))))) % 6.35/6.52 True % 6.35/6.52 Clause #1805 (by clausification #[1804]): ∀ (a a_1 : d), % 6.35/6.52 Eq % 6.35/6.52 (Eq % 6.35/6.52 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.35/6.52 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.52 (s tyop_2Erealax_2Ereal % 6.35/6.52 (c_2Ebinary__ieee_2Eulp_2E1 % 6.35/6.52 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) c_2Ebool_2Ethe__value_2E0))))) % 6.35/6.52 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.52 (s tyop_2Erealax_2Ereal % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.35/6.52 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.35/6.52 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.35/6.52 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) % 6.35/6.52 c_2Ebool_2Ethe__value_2E0))))))))) % 6.35/6.52 False % 6.35/6.52 Clause #1806 (by clausification #[1805]): ∀ (a a_1 : d), % 6.35/6.52 Ne % 6.35/6.52 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.35/6.52 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.52 (s tyop_2Erealax_2Ereal % 6.35/6.52 (c_2Ebinary__ieee_2Eulp_2E1 % 6.35/6.52 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) c_2Ebool_2Ethe__value_2E0))))) % 6.35/6.52 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.52 (s tyop_2Erealax_2Ereal % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.35/6.52 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__negate_2E1 % 6.35/6.52 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.35/6.52 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) % 6.35/6.52 c_2Ebool_2Ethe__value_2E0)))))))) % 6.35/6.52 Clause #1807 (by forward demodulation #[1806, 1616]): ∀ (a a_1 : d), % 6.35/6.52 Ne % 6.35/6.52 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.35/6.52 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.52 (s tyop_2Erealax_2Ereal % 6.35/6.52 (c_2Ebinary__ieee_2Eulp_2E1 % 6.35/6.52 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) c_2Ebool_2Ethe__value_2E0))))) % 6.35/6.52 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.35/6.52 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.52 (s tyop_2Erealax_2Ereal % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__to__real_2E1 % 6.35/6.52 (s (tyop_2Ebinary__ieee_2Efloat (skS.0 2 a) (skS.0 3 a a_1)) % 6.35/6.52 (c_2Ebinary__ieee_2Efloat__plus__min_2E1 % 6.35/6.52 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) % 6.35/6.53 c_2Ebool_2Ethe__value_2E0))))))) % 6.35/6.53 Clause #1808 (by forward demodulation #[1807, 1624]): ∀ (a a_1 : d), % 6.35/6.53 Ne % 6.35/6.53 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.35/6.53 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.53 (s tyop_2Erealax_2Ereal % 6.35/6.53 (c_2Ebinary__ieee_2Eulp_2E1 % 6.35/6.53 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) c_2Ebool_2Ethe__value_2E0))))) % 6.35/6.53 (mono_2Ec_2Erealax_2Ereal__neg_2E1 % 6.35/6.53 (j_mono_2Etyop_2Erealax_2Ereal % 6.35/6.53 (s tyop_2Erealax_2Ereal % 6.35/6.53 (c_2Ebinary__ieee_2Eulp_2E1 % 6.35/6.53 (s (tyop_2Ebool_2Eitself (tyop_2Epair_2Eprod (skS.0 2 a) (skS.0 3 a a_1))) c_2Ebool_2Ethe__value_2E0))))) % 6.35/6.53 Clause #1809 (by eliminate resolved literals #[1808]): False % 6.35/6.53 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------