Z3---4.15.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : Z3---4.15.1
% Problem  : ITP018+2 : TPTP v9.0.0. Bugfixed v7.5.0.
% Transfm  : none
% Format   : tptp
% Command  : run_E %s %d THM

% 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 : Sat Jun 21 05:11:28 AM UTC 2025

% Result   : Theorem 0.74s 0.90s
% Output   : Proof 0.74s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.14  % Problem    : ITP018+2 : TPTP v9.0.0. Bugfixed v7.5.0.
% 0.12/0.14  % Command    : run_E %s %d THM
% 0.13/0.35  % Computer : n003.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 Jun 19 18:18:09 EDT 2025
% 0.13/0.35  % CPUTime    : 
% 0.74/0.90  % SZS status Theorem
% 0.74/0.90  % SZS output start Proof
% 0.74/0.90  tff(ap_type, type, (
% 0.74/0.90     ap: ( $i * $i ) > $i)).
% 0.74/0.90  tff(c_2Ebool_2Ethe__value_type, type, (
% 0.74/0.90     c_2Ebool_2Ethe__value: $i > $i)).
% 0.74/0.90  tff(ty_2Epair_2Eprod_type, type, (
% 0.74/0.90     ty_2Epair_2Eprod: ( $i * $i ) > $i)).
% 0.74/0.90  tff(tptp_fun_A_27w_3_type, type, (
% 0.74/0.90     tptp_fun_A_27w_3: $i)).
% 0.74/0.90  tff(tptp_fun_A_27t_2_type, type, (
% 0.74/0.90     tptp_fun_A_27t_2: $i)).
% 0.74/0.90  tff(c_2Ebinary__ieee_2Efloat__plus__min_type, type, (
% 0.74/0.90     c_2Ebinary__ieee_2Efloat__plus__min: ( $i * $i ) > $i)).
% 0.74/0.90  tff(c_2Ebinary__ieee_2Efloat__to__real_type, type, (
% 0.74/0.90     c_2Ebinary__ieee_2Efloat__to__real: ( $i * $i ) > $i)).
% 0.74/0.90  tff(c_2Erealax_2Ereal__neg_type, type, (
% 0.74/0.90     c_2Erealax_2Ereal__neg: $i)).
% 0.74/0.90  tff(c_2Ebinary__ieee_2Efloat__negate_type, type, (
% 0.74/0.90     c_2Ebinary__ieee_2Efloat__negate: ( $i * $i ) > $i)).
% 0.74/0.90  tff(c_2Ebinary__ieee_2Eulp_type, type, (
% 0.74/0.90     c_2Ebinary__ieee_2Eulp: ( $i * $i ) > $i)).
% 0.74/0.90  tff(ne_type, type, (
% 0.74/0.90     ne: $i > $o)).
% 0.74/0.90  tff(mem_type, type, (
% 0.74/0.90     mem: ( $i * $i ) > $o)).
% 0.74/0.90  tff(ty_2Ebinary__ieee_2Efloat_type, type, (
% 0.74/0.90     ty_2Ebinary__ieee_2Efloat: ( $i * $i ) > $i)).
% 0.74/0.90  tff(ty_2Ebool_2Eitself_type, type, (
% 0.74/0.90     ty_2Ebool_2Eitself: $i > $i)).
% 0.74/0.90  tff(arr_type, type, (
% 0.74/0.90     arr: ( $i * $i ) > $i)).
% 0.74/0.90  tff(1,plain,
% 0.74/0.90      ((ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) <=> (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))))),
% 0.74/0.90      inference(commutativity,[status(thm)],[])).
% 0.74/0.90  tff(2,plain,
% 0.74/0.90      ((~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))))) <=> (~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))))),
% 0.74/0.90      inference(rewrite,[status(thm)],[])).
% 0.74/0.90  tff(3,plain,
% 0.74/0.90      ((~![A_27t: $i] : (ne(A_27t) => ![A_27w: $i] : (ne(A_27w) => (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))))) <=> (~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))))),
% 0.74/0.90      inference(rewrite,[status(thm)],[])).
% 0.74/0.90  tff(4,axiom,(~![A_27t: $i] : (ne(A_27t) => ![A_27w: $i] : (ne(A_27w) => (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','conj_thm_2Ebinary__ieee_2Eneg__ulp')).
% 0.74/0.90  tff(5,plain,
% 0.74/0.90      (~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[4, 3])).
% 0.74/0.90  tff(6,plain,
% 0.74/0.90      (~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[5, 2])).
% 0.74/0.90  tff(7,plain,
% 0.74/0.90      (~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[6, 2])).
% 0.74/0.90  tff(8,plain,
% 0.74/0.90      (~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[7, 2])).
% 0.74/0.90  tff(9,plain,
% 0.74/0.90      (ne(A_27t!2)),
% 0.74/0.90      inference(and_elim,[status(thm)],[8])).
% 0.74/0.90  tff(10,plain,
% 0.74/0.90      (^[A_27t: $i] : refl(((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))) <=> ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))))),
% 0.74/0.90      inference(bind,[status(th)],[])).
% 0.74/0.90  tff(11,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))) <=> ![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))),
% 0.74/0.90      inference(quant_intro,[status(thm)],[10])).
% 0.74/0.90  tff(12,plain,
% 0.74/0.90      (^[A_27t: $i] : rewrite(((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))) <=> ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))))),
% 0.74/0.90      inference(bind,[status(th)],[])).
% 0.74/0.90  tff(13,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))) <=> ![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))),
% 0.74/0.90      inference(quant_intro,[status(thm)],[12])).
% 0.74/0.90  tff(14,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))) <=> ![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))),
% 0.74/0.90      inference(transitivity,[status(thm)],[13, 11])).
% 0.74/0.90  tff(15,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))) <=> ![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))),
% 0.74/0.90      inference(rewrite,[status(thm)],[])).
% 0.74/0.90  tff(16,plain,
% 0.74/0.90      (^[A_27t: $i] : trans(monotonicity(quant_intro(proof_bind(^[A_27w: $i] : rewrite((ne(A_27w) => (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))) <=> ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))), (![A_27w: $i] : (ne(A_27w) => (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))) <=> ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))), ((ne(A_27t) => ![A_27w: $i] : (ne(A_27w) => (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))) <=> (ne(A_27t) => ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))))), rewrite((ne(A_27t) => ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))) <=> ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))), ((ne(A_27t) => ![A_27w: $i] : (ne(A_27w) => (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))) <=> ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))))),
% 0.74/0.90      inference(bind,[status(th)],[])).
% 0.74/0.90  tff(17,plain,
% 0.74/0.90      (![A_27t: $i] : (ne(A_27t) => ![A_27w: $i] : (ne(A_27w) => (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))))))) <=> ![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))),
% 0.74/0.90      inference(quant_intro,[status(thm)],[16])).
% 0.74/0.90  tff(18,axiom,(![A_27t: $i] : (ne(A_27t) => ![A_27w: $i] : (ne(A_27w) => (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','conj_thm_2Ebinary__ieee_2Eulp')).
% 0.74/0.90  tff(19,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[18, 17])).
% 0.74/0.90  tff(20,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[19, 15])).
% 0.74/0.90  tff(21,plain,(
% 0.74/0.90      ![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))),
% 0.74/0.90      inference(skolemize,[status(sab)],[20])).
% 0.74/0.90  tff(22,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[21, 14])).
% 0.74/0.90  tff(23,plain,
% 0.74/0.90      (((~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))) | ((~ne(A_27t!2)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w)))))))) <=> ((~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))) | (~ne(A_27t!2)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w)))))))),
% 0.74/0.90      inference(rewrite,[status(thm)],[])).
% 0.74/0.90  tff(24,plain,
% 0.74/0.90      ((~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))) | ((~ne(A_27t!2)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w)))))))),
% 0.74/0.90      inference(quant_inst,[status(thm)],[])).
% 0.74/0.90  tff(25,plain,
% 0.74/0.90      ((~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t, A_27w)))))))) | (~ne(A_27t!2)) | ![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[24, 23])).
% 0.74/0.90  tff(26,plain,
% 0.74/0.90      (![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))))))),
% 0.74/0.90      inference(unit_resolution,[status(thm)],[25, 22, 9])).
% 0.74/0.90  tff(27,plain,
% 0.74/0.90      (~((~ne(A_27w!3)) | (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))))))),
% 0.74/0.90      inference(and_elim,[status(thm)],[8])).
% 0.74/0.90  tff(28,plain,
% 0.74/0.90      (ne(A_27w!3)),
% 0.74/0.90      inference(or_elim,[status(thm)],[27])).
% 0.74/0.90  tff(29,plain,
% 0.74/0.90      (((~![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))))))) | ((~ne(A_27w!3)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))))) <=> ((~![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))))))) | (~ne(A_27w!3)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))))),
% 0.74/0.90      inference(rewrite,[status(thm)],[])).
% 0.74/0.90  tff(30,plain,
% 0.74/0.90      ((~![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))))))) | ((~ne(A_27w!3)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))))),
% 0.74/0.90      inference(quant_inst,[status(thm)],[])).
% 0.74/0.90  tff(31,plain,
% 0.74/0.90      ((~![A_27w: $i] : ((~ne(A_27w)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w))))))) | (~ne(A_27w!3)) | (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[30, 29])).
% 0.74/0.90  tff(32,plain,
% 0.74/0.90      (ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))),
% 0.74/0.90      inference(unit_resolution,[status(thm)],[31, 28, 26])).
% 0.74/0.90  tff(33,plain,
% 0.74/0.90      (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) = ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))),
% 0.74/0.90      inference(symmetry,[status(thm)],[32])).
% 0.74/0.90  tff(34,plain,
% 0.74/0.90      (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))),
% 0.74/0.90      inference(monotonicity,[status(thm)],[33])).
% 0.74/0.90  tff(35,plain,
% 0.74/0.90      ((ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))))) <=> (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))))),
% 0.74/0.90      inference(monotonicity,[status(thm)],[34])).
% 0.74/0.90  tff(36,plain,
% 0.74/0.90      ((ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))))) <=> (ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))))),
% 0.74/0.90      inference(transitivity,[status(thm)],[35, 1])).
% 0.74/0.90  tff(37,plain,
% 0.74/0.90      ((ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))))) <=> (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))))),
% 0.74/0.90      inference(symmetry,[status(thm)],[36])).
% 0.74/0.90  tff(38,plain,
% 0.74/0.90      ((~(ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))))) <=> (~(ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))))))),
% 0.74/0.90      inference(monotonicity,[status(thm)],[37])).
% 0.74/0.90  tff(39,plain,
% 0.74/0.90      (~(ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Eulp(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))))),
% 0.74/0.90      inference(or_elim,[status(thm)],[27])).
% 0.74/0.90  tff(40,plain,
% 0.74/0.90      (~(ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[39, 38])).
% 0.74/0.90  tff(41,plain,
% 0.74/0.90      (^[A_27t: $i] : refl(((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))) <=> ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))))),
% 0.74/0.90      inference(bind,[status(th)],[])).
% 0.74/0.90  tff(42,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))) <=> ![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))),
% 0.74/0.90      inference(quant_intro,[status(thm)],[41])).
% 0.74/0.90  tff(43,plain,
% 0.74/0.90      (^[A_27t: $i] : rewrite(((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))) <=> ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))))),
% 0.74/0.90      inference(bind,[status(th)],[])).
% 0.74/0.90  tff(44,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))) <=> ![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))),
% 0.74/0.90      inference(quant_intro,[status(thm)],[43])).
% 0.74/0.90  tff(45,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))) <=> ![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))),
% 0.74/0.90      inference(transitivity,[status(thm)],[44, 42])).
% 0.74/0.90  tff(46,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))) <=> ![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))),
% 0.74/0.90      inference(rewrite,[status(thm)],[])).
% 0.74/0.90  tff(47,plain,
% 0.74/0.90      (^[A_27t: $i] : trans(monotonicity(quant_intro(proof_bind(^[A_27w: $i] : rewrite((ne(A_27w) => mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))) <=> ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))), (![A_27w: $i] : (ne(A_27w) => mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))) <=> ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))), ((ne(A_27t) => ![A_27w: $i] : (ne(A_27w) => mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))) <=> (ne(A_27t) => ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))))), rewrite((ne(A_27t) => ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))) <=> ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))), ((ne(A_27t) => ![A_27w: $i] : (ne(A_27w) => mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))) <=> ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))))),
% 0.74/0.90      inference(bind,[status(th)],[])).
% 0.74/0.90  tff(48,plain,
% 0.74/0.90      (![A_27t: $i] : (ne(A_27t) => ![A_27w: $i] : (ne(A_27w) => mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w))))) <=> ![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))),
% 0.74/0.90      inference(quant_intro,[status(thm)],[47])).
% 0.74/0.90  tff(49,axiom,(![A_27t: $i] : (ne(A_27t) => ![A_27w: $i] : (ne(A_27w) => mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mem_c_2Ebinary__ieee_2Efloat__plus__min')).
% 0.74/0.90  tff(50,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[49, 48])).
% 0.74/0.90  tff(51,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[50, 46])).
% 0.74/0.90  tff(52,plain,(
% 0.74/0.90      ![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))),
% 0.74/0.90      inference(skolemize,[status(sab)],[51])).
% 0.74/0.90  tff(53,plain,
% 0.74/0.90      (![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[52, 45])).
% 0.74/0.90  tff(54,plain,
% 0.74/0.90      (((~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))) | ((~ne(A_27t!2)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w)))))) <=> ((~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))) | (~ne(A_27t!2)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w)))))),
% 0.74/0.90      inference(rewrite,[status(thm)],[])).
% 0.74/0.90  tff(55,plain,
% 0.74/0.90      ((~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))) | ((~ne(A_27t!2)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w)))))),
% 0.74/0.90      inference(quant_inst,[status(thm)],[])).
% 0.74/0.90  tff(56,plain,
% 0.74/0.90      ((~![A_27t: $i] : ((~ne(A_27t)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t, A_27w)))))) | (~ne(A_27t!2)) | ![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w))))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[55, 54])).
% 0.74/0.90  tff(57,plain,
% 0.74/0.90      (![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w))))),
% 0.74/0.90      inference(unit_resolution,[status(thm)],[56, 53, 9])).
% 0.74/0.90  tff(58,plain,
% 0.74/0.90      (((~![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w))))) | ((~ne(A_27w!3)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))))) <=> ((~![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w))))) | (~ne(A_27w!3)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))))),
% 0.74/0.90      inference(rewrite,[status(thm)],[])).
% 0.74/0.90  tff(59,plain,
% 0.74/0.90      ((~![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w))))) | ((~ne(A_27w!3)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))))),
% 0.74/0.90      inference(quant_inst,[status(thm)],[])).
% 0.74/0.90  tff(60,plain,
% 0.74/0.90      ((~![A_27w: $i] : ((~ne(A_27w)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w))))) | (~ne(A_27w!3)) | mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))),
% 0.74/0.90      inference(modus_ponens,[status(thm)],[59, 58])).
% 0.74/0.90  tff(61,plain,
% 0.74/0.90      (mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))),
% 0.74/0.90      inference(unit_resolution,[status(thm)],[60, 28, 57])).
% 0.74/0.90  tff(62,plain,
% 0.74/0.90      (^[A: $i, B: $i, F: $i] : refl(((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B))) <=> ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B))))),
% 0.74/0.90      inference(bind,[status(th)],[])).
% 0.74/0.90  tff(63,plain,
% 0.74/0.90      (![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B))) <=> ![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))),
% 0.74/0.90      inference(quant_intro,[status(thm)],[62])).
% 0.74/0.90  tff(64,plain,
% 0.74/0.90      (^[A: $i, B: $i, F: $i] : rewrite(((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B))) <=> ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B))))),
% 0.74/0.90      inference(bind,[status(th)],[])).
% 0.74/0.90  tff(65,plain,
% 0.74/0.90      (![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B))) <=> ![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))),
% 0.74/0.90      inference(quant_intro,[status(thm)],[64])).
% 0.74/0.90  tff(66,plain,
% 0.74/0.90      (![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B))) <=> ![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))),
% 0.74/0.91      inference(transitivity,[status(thm)],[65, 63])).
% 0.74/0.91  tff(67,plain,
% 0.74/0.91      (![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B))) <=> ![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))),
% 0.74/0.91      inference(rewrite,[status(thm)],[])).
% 0.74/0.91  tff(68,plain,
% 0.74/0.91      (^[A: $i, B: $i, F: $i] : trans(monotonicity(quant_intro(proof_bind(^[X: $i] : rewrite((mem(X, A) => mem(ap(F, X), B)) <=> ((~mem(X, A)) | mem(ap(F, X), B)))), (![X: $i] : (mem(X, A) => mem(ap(F, X), B)) <=> ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))), ((mem(F, arr(A, B)) => ![X: $i] : (mem(X, A) => mem(ap(F, X), B))) <=> (mem(F, arr(A, B)) => ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B))))), rewrite((mem(F, arr(A, B)) => ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B))) <=> ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))), ((mem(F, arr(A, B)) => ![X: $i] : (mem(X, A) => mem(ap(F, X), B))) <=> ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))))),
% 0.74/0.91      inference(bind,[status(th)],[])).
% 0.74/0.91  tff(69,plain,
% 0.74/0.91      (![A: $i, B: $i, F: $i] : (mem(F, arr(A, B)) => ![X: $i] : (mem(X, A) => mem(ap(F, X), B))) <=> ![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))),
% 0.74/0.91      inference(quant_intro,[status(thm)],[68])).
% 0.74/0.91  tff(70,axiom,(![A: $i, B: $i, F: $i] : (mem(F, arr(A, B)) => ![X: $i] : (mem(X, A) => mem(ap(F, X), B)))), file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax','ap_tp')).
% 0.74/0.91  tff(71,plain,
% 0.74/0.91      (![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[70, 69])).
% 0.74/0.91  tff(72,plain,
% 0.74/0.91      (![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[71, 67])).
% 0.74/0.91  tff(73,plain,(
% 0.74/0.91      ![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))),
% 0.74/0.91      inference(skolemize,[status(sab)],[72])).
% 0.74/0.91  tff(74,plain,
% 0.74/0.91      (![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[73, 66])).
% 0.74/0.91  tff(75,plain,
% 0.74/0.91      (((~![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))) | ((~mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))) | ![X: $i] : ((~mem(X, ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), X), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))))) <=> ((~![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))) | (~mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))) | ![X: $i] : ((~mem(X, ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), X), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))))),
% 0.74/0.91      inference(rewrite,[status(thm)],[])).
% 0.74/0.91  tff(76,plain,
% 0.74/0.91      ((~![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))) | ((~mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))) | ![X: $i] : ((~mem(X, ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), X), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))))),
% 0.74/0.91      inference(quant_inst,[status(thm)],[])).
% 0.74/0.91  tff(77,plain,
% 0.74/0.91      ((~![A: $i, B: $i, F: $i] : ((~mem(F, arr(A, B))) | ![X: $i] : ((~mem(X, A)) | mem(ap(F, X), B)))) | (~mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))) | ![X: $i] : ((~mem(X, ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), X), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[76, 75])).
% 0.74/0.91  tff(78,plain,
% 0.74/0.91      (![X: $i] : ((~mem(X, ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), X), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))),
% 0.74/0.91      inference(unit_resolution,[status(thm)],[77, 74, 61])).
% 0.74/0.91  tff(79,plain,
% 0.74/0.91      (^[A0: $i] : refl(((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1)))) <=> ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1)))))),
% 0.74/0.91      inference(bind,[status(th)],[])).
% 0.74/0.91  tff(80,plain,
% 0.74/0.91      (![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1)))) <=> ![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))),
% 0.74/0.91      inference(quant_intro,[status(thm)],[79])).
% 0.74/0.91  tff(81,plain,
% 0.74/0.91      (^[A0: $i] : rewrite(((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1)))) <=> ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1)))))),
% 0.74/0.91      inference(bind,[status(th)],[])).
% 0.74/0.91  tff(82,plain,
% 0.74/0.91      (![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1)))) <=> ![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))),
% 0.74/0.91      inference(quant_intro,[status(thm)],[81])).
% 0.74/0.91  tff(83,plain,
% 0.74/0.91      (![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1)))) <=> ![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))),
% 0.74/0.91      inference(transitivity,[status(thm)],[82, 80])).
% 0.74/0.91  tff(84,plain,
% 0.74/0.91      (![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1)))) <=> ![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))),
% 0.74/0.91      inference(rewrite,[status(thm)],[])).
% 0.74/0.91  tff(85,plain,
% 0.74/0.91      (^[A0: $i] : trans(monotonicity(quant_intro(proof_bind(^[A1: $i] : rewrite((ne(A1) => ne(ty_2Epair_2Eprod(A0, A1))) <=> (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))), (![A1: $i] : (ne(A1) => ne(ty_2Epair_2Eprod(A0, A1))) <=> ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))), ((ne(A0) => ![A1: $i] : (ne(A1) => ne(ty_2Epair_2Eprod(A0, A1)))) <=> (ne(A0) => ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1)))))), rewrite((ne(A0) => ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1)))) <=> ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))), ((ne(A0) => ![A1: $i] : (ne(A1) => ne(ty_2Epair_2Eprod(A0, A1)))) <=> ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))))),
% 0.74/0.91      inference(bind,[status(th)],[])).
% 0.74/0.91  tff(86,plain,
% 0.74/0.91      (![A0: $i] : (ne(A0) => ![A1: $i] : (ne(A1) => ne(ty_2Epair_2Eprod(A0, A1)))) <=> ![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))),
% 0.74/0.91      inference(quant_intro,[status(thm)],[85])).
% 0.74/0.91  tff(87,axiom,(![A0: $i] : (ne(A0) => ![A1: $i] : (ne(A1) => ne(ty_2Epair_2Eprod(A0, A1))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','ne_ty_2Epair_2Eprod')).
% 0.74/0.91  tff(88,plain,
% 0.74/0.91      (![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[87, 86])).
% 0.74/0.91  tff(89,plain,
% 0.74/0.91      (![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[88, 84])).
% 0.74/0.91  tff(90,plain,(
% 0.74/0.91      ![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))),
% 0.74/0.91      inference(skolemize,[status(sab)],[89])).
% 0.74/0.91  tff(91,plain,
% 0.74/0.91      (![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[90, 83])).
% 0.74/0.91  tff(92,plain,
% 0.74/0.91      (((~![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))) | ((~ne(A_27t!2)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A_27t!2, A1)) | (~ne(A1))))) <=> ((~![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))) | (~ne(A_27t!2)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A_27t!2, A1)) | (~ne(A1))))),
% 0.74/0.91      inference(rewrite,[status(thm)],[])).
% 0.74/0.91  tff(93,plain,
% 0.74/0.91      ((~![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))) | ((~ne(A_27t!2)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A_27t!2, A1)) | (~ne(A1))))),
% 0.74/0.91      inference(quant_inst,[status(thm)],[])).
% 0.74/0.91  tff(94,plain,
% 0.74/0.91      ((~![A0: $i] : ((~ne(A0)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A0, A1)) | (~ne(A1))))) | (~ne(A_27t!2)) | ![A1: $i] : (ne(ty_2Epair_2Eprod(A_27t!2, A1)) | (~ne(A1)))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[93, 92])).
% 0.74/0.91  tff(95,plain,
% 0.74/0.91      (![A1: $i] : (ne(ty_2Epair_2Eprod(A_27t!2, A1)) | (~ne(A1)))),
% 0.74/0.91      inference(unit_resolution,[status(thm)],[94, 91, 9])).
% 0.74/0.91  tff(96,plain,
% 0.74/0.91      (((~![A1: $i] : (ne(ty_2Epair_2Eprod(A_27t!2, A1)) | (~ne(A1)))) | (ne(ty_2Epair_2Eprod(A_27t!2, A_27w!3)) | (~ne(A_27w!3)))) <=> ((~![A1: $i] : (ne(ty_2Epair_2Eprod(A_27t!2, A1)) | (~ne(A1)))) | ne(ty_2Epair_2Eprod(A_27t!2, A_27w!3)) | (~ne(A_27w!3)))),
% 0.74/0.91      inference(rewrite,[status(thm)],[])).
% 0.74/0.91  tff(97,plain,
% 0.74/0.91      ((~![A1: $i] : (ne(ty_2Epair_2Eprod(A_27t!2, A1)) | (~ne(A1)))) | (ne(ty_2Epair_2Eprod(A_27t!2, A_27w!3)) | (~ne(A_27w!3)))),
% 0.74/0.91      inference(quant_inst,[status(thm)],[])).
% 0.74/0.91  tff(98,plain,
% 0.74/0.91      ((~![A1: $i] : (ne(ty_2Epair_2Eprod(A_27t!2, A1)) | (~ne(A1)))) | ne(ty_2Epair_2Eprod(A_27t!2, A_27w!3)) | (~ne(A_27w!3))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[97, 96])).
% 0.74/0.91  tff(99,plain,
% 0.74/0.91      (ne(ty_2Epair_2Eprod(A_27t!2, A_27w!3))),
% 0.74/0.91      inference(unit_resolution,[status(thm)],[98, 28, 95])).
% 0.74/0.91  tff(100,plain,
% 0.74/0.91      (^[A_27a: $i] : refl(((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a))) <=> ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a))))),
% 0.74/0.91      inference(bind,[status(th)],[])).
% 0.74/0.91  tff(101,plain,
% 0.74/0.91      (![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a))) <=> ![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a)))),
% 0.74/0.91      inference(quant_intro,[status(thm)],[100])).
% 0.74/0.91  tff(102,plain,
% 0.74/0.91      (![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a))) <=> ![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a)))),
% 0.74/0.91      inference(rewrite,[status(thm)],[])).
% 0.74/0.91  tff(103,plain,
% 0.74/0.91      (^[A_27a: $i] : rewrite((ne(A_27a) => mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a))) <=> ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a))))),
% 0.74/0.91      inference(bind,[status(th)],[])).
% 0.74/0.91  tff(104,plain,
% 0.74/0.91      (![A_27a: $i] : (ne(A_27a) => mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a))) <=> ![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a)))),
% 0.74/0.91      inference(quant_intro,[status(thm)],[103])).
% 0.74/0.91  tff(105,axiom,(![A_27a: $i] : (ne(A_27a) => mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mem_c_2Ebool_2Ethe__value')).
% 0.74/0.91  tff(106,plain,
% 0.74/0.91      (![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a)))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[105, 104])).
% 0.74/0.91  tff(107,plain,
% 0.74/0.91      (![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a)))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[106, 102])).
% 0.74/0.91  tff(108,plain,(
% 0.74/0.91      ![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a)))),
% 0.74/0.91      inference(skolemize,[status(sab)],[107])).
% 0.74/0.91  tff(109,plain,
% 0.74/0.91      (![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a)))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[108, 101])).
% 0.74/0.91  tff(110,plain,
% 0.74/0.91      (((~![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a)))) | ((~ne(ty_2Epair_2Eprod(A_27t!2, A_27w!3))) | mem(c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) <=> ((~![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a)))) | (~ne(ty_2Epair_2Eprod(A_27t!2, A_27w!3))) | mem(c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))),
% 0.74/0.91      inference(rewrite,[status(thm)],[])).
% 0.74/0.91  tff(111,plain,
% 0.74/0.91      ((~![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a)))) | ((~ne(ty_2Epair_2Eprod(A_27t!2, A_27w!3))) | mem(c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))),
% 0.74/0.91      inference(quant_inst,[status(thm)],[])).
% 0.74/0.91  tff(112,plain,
% 0.74/0.91      ((~![A_27a: $i] : ((~ne(A_27a)) | mem(c_2Ebool_2Ethe__value(A_27a), ty_2Ebool_2Eitself(A_27a)))) | (~ne(ty_2Epair_2Eprod(A_27t!2, A_27w!3))) | mem(c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[111, 110])).
% 0.74/0.91  tff(113,plain,
% 0.74/0.91      ((~ne(ty_2Epair_2Eprod(A_27t!2, A_27w!3))) | mem(c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))),
% 0.74/0.91      inference(unit_resolution,[status(thm)],[112, 109])).
% 0.74/0.91  tff(114,plain,
% 0.74/0.91      (mem(c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))),
% 0.74/0.91      inference(unit_resolution,[status(thm)],[113, 99])).
% 0.74/0.91  tff(115,plain,
% 0.74/0.91      (((~![X: $i] : ((~mem(X, ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), X), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))) | ((~mem(c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))) <=> ((~![X: $i] : ((~mem(X, ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), X), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))) | (~mem(c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))),
% 0.74/0.91      inference(rewrite,[status(thm)],[])).
% 0.74/0.91  tff(116,plain,
% 0.74/0.91      ((~![X: $i] : ((~mem(X, ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), X), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))) | ((~mem(c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))),
% 0.74/0.91      inference(quant_inst,[status(thm)],[])).
% 0.74/0.91  tff(117,plain,
% 0.74/0.91      ((~![X: $i] : ((~mem(X, ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), X), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3)))) | (~mem(c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)), ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))) | mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[116, 115])).
% 0.74/0.91  tff(118,plain,
% 0.74/0.91      (mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))),
% 0.74/0.91      inference(unit_resolution,[status(thm)],[117, 114, 78])).
% 0.74/0.91  tff(119,plain,
% 0.74/0.91      (^[A_27a: $i] : refl(((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))) <=> ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))))),
% 0.74/0.91      inference(bind,[status(th)],[])).
% 0.74/0.91  tff(120,plain,
% 0.74/0.91      (![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))) <=> ![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))),
% 0.74/0.91      inference(quant_intro,[status(thm)],[119])).
% 0.74/0.91  tff(121,plain,
% 0.74/0.91      (^[A_27a: $i] : rewrite(((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))) <=> ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))))),
% 0.74/0.91      inference(bind,[status(th)],[])).
% 0.74/0.91  tff(122,plain,
% 0.74/0.91      (![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))) <=> ![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))),
% 0.74/0.91      inference(quant_intro,[status(thm)],[121])).
% 0.74/0.91  tff(123,plain,
% 0.74/0.91      (![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))) <=> ![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))),
% 0.74/0.91      inference(transitivity,[status(thm)],[122, 120])).
% 0.74/0.91  tff(124,plain,
% 0.74/0.91      (![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))) <=> ![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))),
% 0.74/0.91      inference(rewrite,[status(thm)],[])).
% 0.74/0.91  tff(125,plain,
% 0.74/0.91      (^[A_27a: $i] : trans(monotonicity(quant_intro(proof_bind(^[A_27b: $i] : trans(monotonicity(quant_intro(proof_bind(^[V0x: $i] : rewrite((mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b)) => (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))) <=> ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))), (![V0x: $i] : (mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b)) => (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))) <=> ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))), ((ne(A_27b) => ![V0x: $i] : (mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b)) => (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))) <=> (ne(A_27b) => ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))), rewrite((ne(A_27b) => ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))) <=> ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))), ((ne(A_27b) => ![V0x: $i] : (mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b)) => (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))) <=> ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))))), (![A_27b: $i] : (ne(A_27b) => ![V0x: $i] : (mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b)) => (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))) <=> ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))), ((ne(A_27a) => ![A_27b: $i] : (ne(A_27b) => ![V0x: $i] : (mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b)) => (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))) <=> (ne(A_27a) => ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))))), rewrite((ne(A_27a) => ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))) <=> ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))), ((ne(A_27a) => ![A_27b: $i] : (ne(A_27b) => ![V0x: $i] : (mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b)) => (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))) <=> ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))))),
% 0.74/0.91      inference(bind,[status(th)],[])).
% 0.74/0.91  tff(126,plain,
% 0.74/0.91      (![A_27a: $i] : (ne(A_27a) => ![A_27b: $i] : (ne(A_27b) => ![V0x: $i] : (mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b)) => (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x)))))) <=> ![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))),
% 0.74/0.91      inference(quant_intro,[status(thm)],[125])).
% 0.74/0.91  tff(127,axiom,(![A_27a: $i] : (ne(A_27a) => ![A_27b: $i] : (ne(A_27b) => ![V0x: $i] : (mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b)) => (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','conj_thm_2Ebinary__ieee_2Efloat__to__real__negate')).
% 0.74/0.91  tff(128,plain,
% 0.74/0.91      (![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[127, 126])).
% 0.74/0.91  tff(129,plain,
% 0.74/0.91      (![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[128, 124])).
% 0.74/0.91  tff(130,plain,(
% 0.74/0.91      ![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))),
% 0.74/0.91      inference(skolemize,[status(sab)],[129])).
% 0.74/0.91  tff(131,plain,
% 0.74/0.91      (![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[130, 123])).
% 0.74/0.91  tff(132,plain,
% 0.74/0.91      (((~![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))) | ((~ne(A_27t!2)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), V0x))))))) <=> ((~![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))) | (~ne(A_27t!2)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), V0x))))))),
% 0.74/0.91      inference(rewrite,[status(thm)],[])).
% 0.74/0.91  tff(133,plain,
% 0.74/0.91      ((~![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))) | ((~ne(A_27t!2)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), V0x))))))),
% 0.74/0.91      inference(quant_inst,[status(thm)],[])).
% 0.74/0.91  tff(134,plain,
% 0.74/0.91      ((~![A_27a: $i] : ((~ne(A_27a)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27a, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27a, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a, A_27b), V0x))))))) | (~ne(A_27t!2)) | ![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), V0x)))))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[133, 132])).
% 0.74/0.91  tff(135,plain,
% 0.74/0.91      (![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), V0x)))))),
% 0.74/0.91      inference(unit_resolution,[status(thm)],[134, 131, 9])).
% 0.74/0.91  tff(136,plain,
% 0.74/0.91      (((~![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), V0x)))))) | ((~ne(A_27w!3)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), V0x)))))) <=> ((~![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), V0x)))))) | (~ne(A_27w!3)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), V0x)))))),
% 0.74/0.91      inference(rewrite,[status(thm)],[])).
% 0.74/0.91  tff(137,plain,
% 0.74/0.91      ((~![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), V0x)))))) | ((~ne(A_27w!3)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), V0x)))))),
% 0.74/0.91      inference(quant_inst,[status(thm)],[])).
% 0.74/0.91  tff(138,plain,
% 0.74/0.91      ((~![A_27b: $i] : ((~ne(A_27b)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27b))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27b), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27b), V0x)))))) | (~ne(A_27w!3)) | ![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), V0x))))),
% 0.74/0.91      inference(modus_ponens,[status(thm)],[137, 136])).
% 0.74/0.91  tff(139,plain,
% 0.74/0.91      (![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), V0x))))),
% 0.74/0.91      inference(unit_resolution,[status(thm)],[138, 28, 135])).
% 0.74/0.91  tff(140,plain,
% 0.74/0.91      (((~![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), V0x))))) | ((~mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))))))) <=> ((~![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), V0x))))) | (~mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))))))),
% 0.74/0.91      inference(rewrite,[status(thm)],[])).
% 0.74/0.91  tff(141,plain,
% 0.74/0.91      ((~![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), V0x))))) | ((~mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3)))))))),
% 0.74/0.92      inference(quant_inst,[status(thm)],[])).
% 0.74/0.92  tff(142,plain,
% 0.74/0.92      ((~![V0x: $i] : ((~mem(V0x, ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), V0x)) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), V0x))))) | (~mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))))),
% 0.74/0.92      inference(modus_ponens,[status(thm)],[141, 140])).
% 0.74/0.92  tff(143,plain,
% 0.74/0.92      ((~mem(ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))), ty_2Ebinary__ieee_2Efloat(A_27t!2, A_27w!3))) | (ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__negate(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))) = ap(c_2Erealax_2Ereal__neg, ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t!2, A_27w!3), ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t!2, A_27w!3), c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t!2, A_27w!3))))))),
% 0.74/0.92      inference(unit_resolution,[status(thm)],[142, 139])).
% 0.74/0.92  tff(144,plain,
% 0.74/0.92      ($false),
% 0.74/0.92      inference(unit_resolution,[status(thm)],[143, 118, 40])).
% 0.74/0.92  % SZS output end Proof
% 0.74/0.92  % E exiting
%------------------------------------------------------------------------------