%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : GEO526+1 : TPTP v9.0.0. Released v7.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n008.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:06:27 AM UTC 2025
% Result : Theorem 0.70s 0.88s
% Output : Proof 0.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO526+1 : TPTP v9.0.0. Released v7.0.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n008.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu Jun 19 15:01:03 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.70/0.88 % SZS status Theorem
% 0.70/0.88 % SZS output start Proof
% 0.70/0.88 tff(s_r_type, type, (
% 0.70/0.88 s_r: ( $i * $i * $i ) > $o)).
% 0.70/0.88 tff(tptp_fun_Xc_2_type, type, (
% 0.70/0.88 tptp_fun_Xc_2: $i)).
% 0.70/0.88 tff(isomidpoint_type, type, (
% 0.70/0.88 isomidpoint: ( $i * $i * $i ) > $i)).
% 0.70/0.88 tff(midpoint_type, type, (
% 0.70/0.88 midpoint: ( $i * $i ) > $i)).
% 0.70/0.88 tff(tptp_fun_Xc1_0_type, type, (
% 0.70/0.88 tptp_fun_Xc1_0: $i)).
% 0.70/0.88 tff(tptp_fun_Xa_3_type, type, (
% 0.70/0.88 tptp_fun_Xa_3: $i)).
% 0.70/0.88 tff(s_m_type, type, (
% 0.70/0.88 s_m: ( $i * $i * $i ) > $o)).
% 0.70/0.88 tff(s_e_type, type, (
% 0.70/0.88 s_e: ( $i * $i * $i * $i ) > $o)).
% 0.70/0.88 tff(tptp_fun_Xa1_1_type, type, (
% 0.70/0.88 tptp_fun_Xa1_1: $i)).
% 0.70/0.88 tff(s_type, type, (
% 0.70/0.88 s: ( $i * $i ) > $i)).
% 0.70/0.88 tff(1,plain,
% 0.70/0.88 ((~(s_e(Xa!3, Xc!2, Xa1!1, Xc1!0) | (Xc!2 = Xc1!0) | (~s_e(midpoint(Xc!2, Xc1!0), Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_r(Xa!3, midpoint(Xc!2, Xc1!0), Xc!2)) | (~s_e(Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1, midpoint(Xc!2, Xc1!0))))) <=> (~(s_e(Xa!3, Xc!2, Xa1!1, Xc1!0) | (Xc!2 = Xc1!0) | (~s_e(midpoint(Xc!2, Xc1!0), Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_r(Xa!3, midpoint(Xc!2, Xc1!0), Xc!2)) | (~s_e(Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1, midpoint(Xc!2, Xc1!0)))))),
% 0.70/0.88 inference(rewrite,[status(thm)],[])).
% 0.70/0.88 tff(2,plain,
% 0.70/0.88 ((~![Xa: $i, Xc: $i, Xa1: $i, Xc1: $i] : (s_e(Xa, Xc, Xa1, Xc1) | (Xc = Xc1) | (~s_e(midpoint(Xc, Xc1), Xc, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa1, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa, midpoint(Xc, Xc1), Xc)) | (~s_e(Xa, midpoint(Xc, Xc1), Xa1, midpoint(Xc, Xc1))))) <=> (~![Xa: $i, Xc: $i, Xa1: $i, Xc1: $i] : (s_e(Xa, Xc, Xa1, Xc1) | (Xc = Xc1) | (~s_e(midpoint(Xc, Xc1), Xc, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa1, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa, midpoint(Xc, Xc1), Xc)) | (~s_e(Xa, midpoint(Xc, Xc1), Xa1, midpoint(Xc, Xc1)))))),
% 0.70/0.88 inference(rewrite,[status(thm)],[])).
% 0.70/0.88 tff(3,plain,
% 0.70/0.88 ((~![Xa: $i, Xb: $i, Xc: $i, Xa1: $i, Xc1: $i] : (((((((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc1))) | (~s_e(Xa, Xb, Xa1, Xb))) | (~s_e(Xb, Xc, Xb, Xc1))) | s_e(Xa, Xc, Xa1, Xc1)) | (~(Xb = midpoint(Xc, Xc1)))) | (Xc = Xc1))) <=> (~![Xa: $i, Xc: $i, Xa1: $i, Xc1: $i] : (s_e(Xa, Xc, Xa1, Xc1) | (Xc = Xc1) | (~s_e(midpoint(Xc, Xc1), Xc, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa1, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa, midpoint(Xc, Xc1), Xc)) | (~s_e(Xa, midpoint(Xc, Xc1), Xa1, midpoint(Xc, Xc1)))))),
% 0.70/0.88 inference(rewrite,[status(thm)],[])).
% 0.70/0.88 tff(4,axiom,(~![Xa: $i, Xb: $i, Xc: $i, Xa1: $i, Xc1: $i] : (((((((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc1))) | (~s_e(Xa, Xb, Xa1, Xb))) | (~s_e(Xb, Xc, Xb, Xc1))) | s_e(Xa, Xc, Xa1, Xc1)) | (~(Xb = midpoint(Xc, Xc1)))) | (Xc = Xc1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','aSatz10_12c')).
% 0.70/0.88 tff(5,plain,
% 0.70/0.88 (~![Xa: $i, Xc: $i, Xa1: $i, Xc1: $i] : (s_e(Xa, Xc, Xa1, Xc1) | (Xc = Xc1) | (~s_e(midpoint(Xc, Xc1), Xc, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa1, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa, midpoint(Xc, Xc1), Xc)) | (~s_e(Xa, midpoint(Xc, Xc1), Xa1, midpoint(Xc, Xc1))))),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.70/0.88 tff(6,plain,
% 0.70/0.88 (~![Xa: $i, Xc: $i, Xa1: $i, Xc1: $i] : (s_e(Xa, Xc, Xa1, Xc1) | (Xc = Xc1) | (~s_e(midpoint(Xc, Xc1), Xc, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa1, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa, midpoint(Xc, Xc1), Xc)) | (~s_e(Xa, midpoint(Xc, Xc1), Xa1, midpoint(Xc, Xc1))))),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[5, 2])).
% 0.70/0.88 tff(7,plain,
% 0.70/0.88 (~![Xa: $i, Xc: $i, Xa1: $i, Xc1: $i] : (s_e(Xa, Xc, Xa1, Xc1) | (Xc = Xc1) | (~s_e(midpoint(Xc, Xc1), Xc, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa1, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa, midpoint(Xc, Xc1), Xc)) | (~s_e(Xa, midpoint(Xc, Xc1), Xa1, midpoint(Xc, Xc1))))),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[6, 2])).
% 0.70/0.88 tff(8,plain,
% 0.70/0.88 (~![Xa: $i, Xc: $i, Xa1: $i, Xc1: $i] : (s_e(Xa, Xc, Xa1, Xc1) | (Xc = Xc1) | (~s_e(midpoint(Xc, Xc1), Xc, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa1, midpoint(Xc, Xc1), Xc1)) | (~s_r(Xa, midpoint(Xc, Xc1), Xc)) | (~s_e(Xa, midpoint(Xc, Xc1), Xa1, midpoint(Xc, Xc1))))),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[7, 2])).
% 0.70/0.88 tff(9,plain,(
% 0.70/0.88 ~(s_e(Xa!3, Xc!2, Xa1!1, Xc1!0) | (Xc!2 = Xc1!0) | (~s_e(midpoint(Xc!2, Xc1!0), Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_r(Xa!3, midpoint(Xc!2, Xc1!0), Xc!2)) | (~s_e(Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1, midpoint(Xc!2, Xc1!0))))),
% 0.70/0.88 inference(skolemize,[status(sab)],[8])).
% 0.70/0.88 tff(10,plain,
% 0.70/0.88 (~(s_e(Xa!3, Xc!2, Xa1!1, Xc1!0) | (Xc!2 = Xc1!0) | (~s_e(midpoint(Xc!2, Xc1!0), Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_r(Xa!3, midpoint(Xc!2, Xc1!0), Xc!2)) | (~s_e(Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1, midpoint(Xc!2, Xc1!0))))),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[9, 1])).
% 0.70/0.88 tff(11,plain,
% 0.70/0.88 (s_e(midpoint(Xc!2, Xc1!0), Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)),
% 0.70/0.88 inference(or_elim,[status(thm)],[10])).
% 0.70/0.88 tff(12,plain,
% 0.70/0.88 (^[Xc: $i, Xa: $i, Xb: $i] : refl(((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb)) <=> ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb)))),
% 0.70/0.88 inference(bind,[status(th)],[])).
% 0.70/0.88 tff(13,plain,
% 0.70/0.88 (![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb)) <=> ![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))),
% 0.70/0.88 inference(quant_intro,[status(thm)],[12])).
% 0.70/0.88 tff(14,plain,
% 0.70/0.88 (![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb)) <=> ![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))),
% 0.70/0.88 inference(rewrite,[status(thm)],[])).
% 0.70/0.88 tff(15,axiom,(![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','aSatz7_25')).
% 0.70/0.88 tff(16,plain,
% 0.70/0.88 (![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.70/0.88 tff(17,plain,(
% 0.70/0.88 ![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))),
% 0.70/0.88 inference(skolemize,[status(sab)],[16])).
% 0.70/0.88 tff(18,plain,
% 0.70/0.88 (![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[17, 13])).
% 0.70/0.88 tff(19,plain,
% 0.70/0.88 (((~![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))) | ((~s_e(midpoint(Xc!2, Xc1!0), Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0))) <=> ((~![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))) | (~s_e(midpoint(Xc!2, Xc1!0), Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0))),
% 0.70/0.88 inference(rewrite,[status(thm)],[])).
% 0.70/0.88 tff(20,plain,
% 0.70/0.88 ((~![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))) | ((~s_e(midpoint(Xc!2, Xc1!0), Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0))),
% 0.70/0.88 inference(quant_inst,[status(thm)],[])).
% 0.70/0.88 tff(21,plain,
% 0.70/0.88 ((~![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))) | (~s_e(midpoint(Xc!2, Xc1!0), Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[20, 19])).
% 0.70/0.88 tff(22,plain,
% 0.70/0.88 (s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)),
% 0.70/0.88 inference(unit_resolution,[status(thm)],[21, 18, 11])).
% 0.70/0.88 tff(23,plain,
% 0.70/0.88 (^[Xa: $i, Xb: $i] : refl(s_m(Xa, midpoint(Xa, Xb), Xb) <=> s_m(Xa, midpoint(Xa, Xb), Xb))),
% 0.70/0.88 inference(bind,[status(th)],[])).
% 0.70/0.88 tff(24,plain,
% 0.70/0.88 (![Xa: $i, Xb: $i] : s_m(Xa, midpoint(Xa, Xb), Xb) <=> ![Xa: $i, Xb: $i] : s_m(Xa, midpoint(Xa, Xb), Xb)),
% 0.70/0.88 inference(quant_intro,[status(thm)],[23])).
% 0.70/0.88 tff(25,plain,
% 0.70/0.88 (![Xa: $i, Xb: $i] : s_m(Xa, midpoint(Xa, Xb), Xb) <=> ![Xa: $i, Xb: $i] : s_m(Xa, midpoint(Xa, Xb), Xb)),
% 0.70/0.88 inference(rewrite,[status(thm)],[])).
% 0.70/0.88 tff(26,axiom,(![Xa: $i, Xb: $i] : s_m(Xa, midpoint(Xa, Xb), Xb)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','aSatz8_22')).
% 0.70/0.88 tff(27,plain,
% 0.70/0.88 (![Xa: $i, Xb: $i] : s_m(Xa, midpoint(Xa, Xb), Xb)),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[26, 25])).
% 0.70/0.88 tff(28,plain,(
% 0.70/0.88 ![Xa: $i, Xb: $i] : s_m(Xa, midpoint(Xa, Xb), Xb)),
% 0.70/0.88 inference(skolemize,[status(sab)],[27])).
% 0.70/0.88 tff(29,plain,
% 0.70/0.88 (![Xa: $i, Xb: $i] : s_m(Xa, midpoint(Xa, Xb), Xb)),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[28, 24])).
% 0.70/0.88 tff(30,plain,
% 0.70/0.88 ((~![Xa: $i, Xb: $i] : s_m(Xa, midpoint(Xa, Xb), Xb)) | s_m(Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)),
% 0.70/0.88 inference(quant_inst,[status(thm)],[])).
% 0.70/0.88 tff(31,plain,
% 0.70/0.88 (s_m(Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)),
% 0.70/0.88 inference(unit_resolution,[status(thm)],[30, 29])).
% 0.70/0.88 tff(32,plain,
% 0.70/0.88 (^[Xp: $i, Xa: $i, Xq: $i, Xb: $i] : refl(((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq))) <=> ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq))))),
% 0.70/0.88 inference(bind,[status(th)],[])).
% 0.70/0.88 tff(33,plain,
% 0.70/0.88 (![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq))) <=> ![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))),
% 0.70/0.88 inference(quant_intro,[status(thm)],[32])).
% 0.70/0.88 tff(34,plain,
% 0.70/0.88 (![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq))) <=> ![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))),
% 0.70/0.88 inference(rewrite,[status(thm)],[])).
% 0.70/0.88 tff(35,plain,
% 0.70/0.88 (^[Xp: $i, Xa: $i, Xq: $i, Xb: $i] : trans(monotonicity(rewrite(((~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq))) <=> ((~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))), ((((~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq))) | (Xa = Xb)) <=> (((~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq))) | (Xa = Xb)))), rewrite((((~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq))) | (Xa = Xb)) <=> ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))), ((((~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq))) | (Xa = Xb)) <=> ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))))),
% 0.70/0.88 inference(bind,[status(th)],[])).
% 0.70/0.88 tff(36,plain,
% 0.70/0.88 (![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : (((~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq))) | (Xa = Xb)) <=> ![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))),
% 0.70/0.88 inference(quant_intro,[status(thm)],[35])).
% 0.70/0.88 tff(37,axiom,(![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : (((~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq))) | (Xa = Xb))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','aSatz7_17')).
% 0.70/0.88 tff(38,plain,
% 0.70/0.88 (![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[37, 36])).
% 0.70/0.88 tff(39,plain,
% 0.70/0.88 (![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[38, 34])).
% 0.70/0.88 tff(40,plain,(
% 0.70/0.88 ![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))),
% 0.70/0.88 inference(skolemize,[status(sab)],[39])).
% 0.70/0.88 tff(41,plain,
% 0.70/0.88 (![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[40, 33])).
% 0.70/0.88 tff(42,plain,
% 0.70/0.88 (((~![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))) | ((~s_m(Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)) | (midpoint(Xc!2, Xc1!0) = isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0))))) <=> ((~![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))) | (~s_m(Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)) | (midpoint(Xc!2, Xc1!0) = isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0))))),
% 0.70/0.88 inference(rewrite,[status(thm)],[])).
% 0.70/0.88 tff(43,plain,
% 0.70/0.88 (((midpoint(Xc!2, Xc1!0) = isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0))) | (~s_m(Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0))) <=> ((~s_m(Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)) | (midpoint(Xc!2, Xc1!0) = isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0))))),
% 0.70/0.88 inference(rewrite,[status(thm)],[])).
% 0.70/0.88 tff(44,plain,
% 0.70/0.88 (((~![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))) | ((midpoint(Xc!2, Xc1!0) = isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0))) | (~s_m(Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)))) <=> ((~![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))) | ((~s_m(Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)) | (midpoint(Xc!2, Xc1!0) = isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))))),
% 0.70/0.88 inference(monotonicity,[status(thm)],[43])).
% 0.70/0.88 tff(45,plain,
% 0.70/0.88 (((~![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))) | ((midpoint(Xc!2, Xc1!0) = isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0))) | (~s_m(Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)))) <=> ((~![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))) | (~s_m(Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)) | (midpoint(Xc!2, Xc1!0) = isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0))))),
% 0.70/0.88 inference(transitivity,[status(thm)],[44, 42])).
% 0.70/0.88 tff(46,plain,
% 0.70/0.88 ((~![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))) | ((midpoint(Xc!2, Xc1!0) = isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0))) | (~s_m(Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)))),
% 0.70/0.88 inference(quant_inst,[status(thm)],[])).
% 0.70/0.88 tff(47,plain,
% 0.70/0.88 ((~![Xp: $i, Xa: $i, Xq: $i, Xb: $i] : ((Xa = Xb) | (~s_m(Xp, Xa, Xq)) | (~s_m(Xp, Xb, Xq)))) | (~s_m(Xc!2, midpoint(Xc!2, Xc1!0), Xc1!0)) | (~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)) | (midpoint(Xc!2, Xc1!0) = isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[46, 45])).
% 0.70/0.88 tff(48,plain,
% 0.70/0.88 (midpoint(Xc!2, Xc1!0) = isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0))),
% 0.70/0.88 inference(unit_resolution,[status(thm)],[47, 41, 31, 22])).
% 0.70/0.88 tff(49,plain,
% 0.70/0.88 (isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)) = midpoint(Xc!2, Xc1!0)),
% 0.70/0.88 inference(symmetry,[status(thm)],[48])).
% 0.70/0.88 tff(50,plain,
% 0.70/0.88 (s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2) <=> s_r(Xa!3, midpoint(Xc!2, Xc1!0), Xc!2)),
% 0.70/0.88 inference(monotonicity,[status(thm)],[49])).
% 0.70/0.88 tff(51,plain,
% 0.70/0.88 (s_r(Xa!3, midpoint(Xc!2, Xc1!0), Xc!2) <=> s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)),
% 0.70/0.88 inference(symmetry,[status(thm)],[50])).
% 0.70/0.88 tff(52,plain,
% 0.70/0.88 (s_r(Xa!3, midpoint(Xc!2, Xc1!0), Xc!2)),
% 0.70/0.88 inference(or_elim,[status(thm)],[10])).
% 0.70/0.88 tff(53,plain,
% 0.70/0.88 (s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[52, 51])).
% 0.70/0.88 tff(54,plain,
% 0.70/0.88 (s_e(Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1, midpoint(Xc!2, Xc1!0))),
% 0.70/0.88 inference(or_elim,[status(thm)],[10])).
% 0.70/0.88 tff(55,plain,
% 0.70/0.88 (^[Xa: $i, Xb: $i, Xc: $i, Xd: $i] : refl(((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc)) <=> ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc)))),
% 0.70/0.88 inference(bind,[status(th)],[])).
% 0.70/0.88 tff(56,plain,
% 0.70/0.88 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc)) <=> ![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc))),
% 0.70/0.88 inference(quant_intro,[status(thm)],[55])).
% 0.70/0.88 tff(57,plain,
% 0.70/0.88 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc)) <=> ![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc))),
% 0.70/0.88 inference(rewrite,[status(thm)],[])).
% 0.70/0.88 tff(58,axiom,(![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','aSatz2_14')).
% 0.70/0.88 tff(59,plain,
% 0.70/0.88 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc))),
% 0.70/0.88 inference(modus_ponens,[status(thm)],[58, 57])).
% 0.70/0.88 tff(60,plain,(
% 0.70/0.88 ![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc))),
% 0.70/0.89 inference(skolemize,[status(sab)],[59])).
% 0.70/0.89 tff(61,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[60, 56])).
% 0.70/0.89 tff(62,plain,
% 0.70/0.89 (((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc))) | ((~s_e(Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1, midpoint(Xc!2, Xc1!0))) | s_e(midpoint(Xc!2, Xc1!0), Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1))) <=> ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc))) | (~s_e(Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1, midpoint(Xc!2, Xc1!0))) | s_e(midpoint(Xc!2, Xc1!0), Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1))),
% 0.70/0.89 inference(rewrite,[status(thm)],[])).
% 0.70/0.89 tff(63,plain,
% 0.70/0.89 ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc))) | ((~s_e(Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1, midpoint(Xc!2, Xc1!0))) | s_e(midpoint(Xc!2, Xc1!0), Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1))),
% 0.70/0.89 inference(quant_inst,[status(thm)],[])).
% 0.70/0.89 tff(64,plain,
% 0.70/0.89 ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xb, Xa, Xd, Xc))) | (~s_e(Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1, midpoint(Xc!2, Xc1!0))) | s_e(midpoint(Xc!2, Xc1!0), Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1)),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[63, 62])).
% 0.70/0.89 tff(65,plain,
% 0.70/0.89 (s_e(midpoint(Xc!2, Xc1!0), Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1)),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[64, 61, 54])).
% 0.70/0.89 tff(66,plain,
% 0.70/0.89 (((~![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))) | ((~s_e(midpoint(Xc!2, Xc1!0), Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1)) | s_m(Xa!3, isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa1!1))) <=> ((~![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))) | (~s_e(midpoint(Xc!2, Xc1!0), Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1)) | s_m(Xa!3, isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa1!1))),
% 0.70/0.89 inference(rewrite,[status(thm)],[])).
% 0.70/0.89 tff(67,plain,
% 0.70/0.89 ((~![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))) | ((~s_e(midpoint(Xc!2, Xc1!0), Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1)) | s_m(Xa!3, isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa1!1))),
% 0.70/0.89 inference(quant_inst,[status(thm)],[])).
% 0.70/0.89 tff(68,plain,
% 0.70/0.89 ((~![Xc: $i, Xa: $i, Xb: $i] : ((~s_e(Xc, Xa, Xc, Xb)) | s_m(Xa, isomidpoint(Xa, Xb, Xc), Xb))) | (~s_e(midpoint(Xc!2, Xc1!0), Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1)) | s_m(Xa!3, isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa1!1)),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[67, 66])).
% 0.70/0.89 tff(69,plain,
% 0.70/0.89 (s_m(Xa!3, isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa1!1)),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[68, 18, 65])).
% 0.70/0.89 tff(70,plain,
% 0.70/0.89 (^[Xp: $i, Xa: $i, Xq: $i] : refl(((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp))) <=> ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp))))),
% 0.70/0.89 inference(bind,[status(th)],[])).
% 0.70/0.89 tff(71,plain,
% 0.70/0.89 (![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp))) <=> ![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))),
% 0.70/0.89 inference(quant_intro,[status(thm)],[70])).
% 0.70/0.89 tff(72,plain,
% 0.70/0.89 (![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp))) <=> ![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))),
% 0.70/0.89 inference(rewrite,[status(thm)],[])).
% 0.70/0.89 tff(73,axiom,(![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','aSatz7_6')).
% 0.70/0.89 tff(74,plain,
% 0.70/0.89 (![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[73, 72])).
% 0.70/0.89 tff(75,plain,(
% 0.70/0.89 ![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))),
% 0.70/0.89 inference(skolemize,[status(sab)],[74])).
% 0.70/0.89 tff(76,plain,
% 0.70/0.89 (![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[75, 71])).
% 0.70/0.89 tff(77,plain,
% 0.70/0.89 (((~![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))) | ((~s_m(Xa!3, isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa1!1)) | (Xa1!1 = s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3)))) <=> ((~![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))) | (~s_m(Xa!3, isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa1!1)) | (Xa1!1 = s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3)))),
% 0.70/0.89 inference(rewrite,[status(thm)],[])).
% 0.70/0.89 tff(78,plain,
% 0.70/0.89 ((~![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))) | ((~s_m(Xa!3, isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa1!1)) | (Xa1!1 = s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3)))),
% 0.70/0.89 inference(quant_inst,[status(thm)],[])).
% 0.70/0.89 tff(79,plain,
% 0.70/0.89 ((~![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))) | (~s_m(Xa!3, isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa1!1)) | (Xa1!1 = s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[78, 77])).
% 0.70/0.89 tff(80,plain,
% 0.70/0.89 (Xa1!1 = s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3)),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[79, 76, 69])).
% 0.70/0.89 tff(81,plain,
% 0.70/0.89 (s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3) = Xa1!1),
% 0.70/0.89 inference(symmetry,[status(thm)],[80])).
% 0.70/0.89 tff(82,plain,
% 0.70/0.89 (s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0))) <=> s_e(Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1, midpoint(Xc!2, Xc1!0))),
% 0.70/0.89 inference(monotonicity,[status(thm)],[49, 81, 49])).
% 0.70/0.89 tff(83,plain,
% 0.70/0.89 (s_e(Xa!3, midpoint(Xc!2, Xc1!0), Xa1!1, midpoint(Xc!2, Xc1!0)) <=> s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))),
% 0.70/0.89 inference(symmetry,[status(thm)],[82])).
% 0.70/0.89 tff(84,plain,
% 0.70/0.89 (s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[54, 83])).
% 0.70/0.89 tff(85,plain,
% 0.70/0.89 (^[Xa: $i, Xb: $i, Xc: $i] : refl((~((~((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc)))) | (~(s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc))))))) <=> (~((~((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc)))) | (~(s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc))))))))),
% 0.70/0.89 inference(bind,[status(th)],[])).
% 0.70/0.89 tff(86,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i] : (~((~((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc)))) | (~(s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc))))))) <=> ![Xa: $i, Xb: $i, Xc: $i] : (~((~((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc)))) | (~(s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))))))),
% 0.70/0.89 inference(quant_intro,[status(thm)],[85])).
% 0.70/0.89 tff(87,plain,
% 0.70/0.89 (^[Xa: $i, Xb: $i, Xc: $i] : trans(monotonicity(rewrite((s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))) <=> (s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc))))), ((((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc))) & (s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc))))) <=> (((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc))) & (s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc))))))), rewrite((((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc))) & (s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc))))) <=> (~((~((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc)))) | (~(s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))))))), ((((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc))) & (s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc))))) <=> (~((~((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc)))) | (~(s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))))))))),
% 0.70/0.89 inference(bind,[status(th)],[])).
% 0.70/0.89 tff(88,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i] : (((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc))) & (s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc))))) <=> ![Xa: $i, Xb: $i, Xc: $i] : (~((~((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc)))) | (~(s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))))))),
% 0.70/0.89 inference(quant_intro,[status(thm)],[87])).
% 0.70/0.89 tff(89,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i] : (((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc))) & (s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc))))) <=> ![Xa: $i, Xb: $i, Xc: $i] : (((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc))) & (s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))))),
% 0.70/0.89 inference(rewrite,[status(thm)],[])).
% 0.70/0.89 tff(90,axiom,(![Xa: $i, Xb: $i, Xc: $i] : (((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc))) & (s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d_Defn8_1')).
% 0.70/0.89 tff(91,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i] : (((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc))) & (s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[90, 89])).
% 0.70/0.89 tff(92,plain,(
% 0.70/0.89 ![Xa: $i, Xb: $i, Xc: $i] : (((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc))) & (s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))))),
% 0.70/0.89 inference(skolemize,[status(sab)],[91])).
% 0.70/0.89 tff(93,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i] : (~((~((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc)))) | (~(s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))))))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[92, 88])).
% 0.70/0.89 tff(94,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i] : (~((~((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc)))) | (~(s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))))))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[93, 86])).
% 0.70/0.89 tff(95,plain,
% 0.70/0.89 ((~![Xa: $i, Xb: $i, Xc: $i] : (~((~((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc)))) | (~(s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))))))) | (~((~((~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))) | (~(s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2) | (~s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))))))),
% 0.70/0.89 inference(quant_inst,[status(thm)],[])).
% 0.70/0.89 tff(96,plain,
% 0.70/0.89 (~((~((~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))) | (~(s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2) | (~s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))))))),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[95, 94])).
% 0.70/0.89 tff(97,plain,
% 0.70/0.89 (((~((~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))) | (~(s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2) | (~s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))))) | (s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2) | (~s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))))),
% 0.70/0.89 inference(tautology,[status(thm)],[])).
% 0.70/0.89 tff(98,plain,
% 0.70/0.89 (s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2) | (~s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[97, 96])).
% 0.70/0.89 tff(99,plain,
% 0.70/0.89 (s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) <=> s_e(Xa1!1, Xc!2, Xa1!1, s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))),
% 0.70/0.89 inference(monotonicity,[status(thm)],[81, 81])).
% 0.70/0.89 tff(100,plain,
% 0.70/0.89 (s_e(Xa1!1, Xc!2, Xa1!1, s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) <=> s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))),
% 0.70/0.89 inference(symmetry,[status(thm)],[99])).
% 0.70/0.89 tff(101,plain,
% 0.70/0.89 (((~![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))) | ((~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)) | (Xc1!0 = s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))) <=> ((~![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))) | (~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)) | (Xc1!0 = s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))),
% 0.70/0.89 inference(rewrite,[status(thm)],[])).
% 0.70/0.89 tff(102,plain,
% 0.70/0.89 ((~![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))) | ((~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)) | (Xc1!0 = s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))),
% 0.70/0.89 inference(quant_inst,[status(thm)],[])).
% 0.70/0.89 tff(103,plain,
% 0.70/0.89 ((~![Xp: $i, Xa: $i, Xq: $i] : ((~s_m(Xp, Xa, Xq)) | (Xq = s(Xa, Xp)))) | (~s_m(Xc!2, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc1!0)) | (Xc1!0 = s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[102, 101])).
% 0.70/0.89 tff(104,plain,
% 0.70/0.89 (Xc1!0 = s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[103, 76, 22])).
% 0.70/0.89 tff(105,plain,
% 0.70/0.89 (s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2) = Xc1!0),
% 0.70/0.89 inference(symmetry,[status(thm)],[104])).
% 0.70/0.89 tff(106,plain,
% 0.70/0.89 (s(midpoint(Xc!2, Xc1!0), Xc1!0) = s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))),
% 0.70/0.89 inference(monotonicity,[status(thm)],[48, 104])).
% 0.70/0.89 tff(107,plain,
% 0.70/0.89 (s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) = s(midpoint(Xc!2, Xc1!0), Xc1!0)),
% 0.70/0.89 inference(symmetry,[status(thm)],[106])).
% 0.70/0.89 tff(108,plain,
% 0.70/0.89 (^[Xa: $i, Xp: $i] : refl((s(Xa, s(Xa, Xp)) = Xp) <=> (s(Xa, s(Xa, Xp)) = Xp))),
% 0.70/0.89 inference(bind,[status(th)],[])).
% 0.70/0.89 tff(109,plain,
% 0.70/0.89 (![Xa: $i, Xp: $i] : (s(Xa, s(Xa, Xp)) = Xp) <=> ![Xa: $i, Xp: $i] : (s(Xa, s(Xa, Xp)) = Xp)),
% 0.70/0.89 inference(quant_intro,[status(thm)],[108])).
% 0.70/0.89 tff(110,plain,
% 0.70/0.89 (![Xa: $i, Xp: $i] : (s(Xa, s(Xa, Xp)) = Xp) <=> ![Xa: $i, Xp: $i] : (s(Xa, s(Xa, Xp)) = Xp)),
% 0.70/0.89 inference(rewrite,[status(thm)],[])).
% 0.70/0.89 tff(111,axiom,(![Xa: $i, Xp: $i] : (s(Xa, s(Xa, Xp)) = Xp)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','aSatz7_7')).
% 0.70/0.89 tff(112,plain,
% 0.70/0.89 (![Xa: $i, Xp: $i] : (s(Xa, s(Xa, Xp)) = Xp)),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[111, 110])).
% 0.70/0.89 tff(113,plain,(
% 0.70/0.89 ![Xa: $i, Xp: $i] : (s(Xa, s(Xa, Xp)) = Xp)),
% 0.70/0.89 inference(skolemize,[status(sab)],[112])).
% 0.70/0.89 tff(114,plain,
% 0.70/0.89 (![Xa: $i, Xp: $i] : (s(Xa, s(Xa, Xp)) = Xp)),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[113, 109])).
% 0.70/0.89 tff(115,plain,
% 0.70/0.89 ((~![Xa: $i, Xp: $i] : (s(Xa, s(Xa, Xp)) = Xp)) | (s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) = Xc!2)),
% 0.70/0.89 inference(quant_inst,[status(thm)],[])).
% 0.70/0.89 tff(116,plain,
% 0.70/0.89 (s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) = Xc!2),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[115, 114])).
% 0.70/0.89 tff(117,plain,
% 0.70/0.89 (Xc!2 = s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))),
% 0.70/0.89 inference(symmetry,[status(thm)],[116])).
% 0.70/0.89 tff(118,plain,
% 0.70/0.89 (Xc!2 = s(midpoint(Xc!2, Xc1!0), Xc1!0)),
% 0.70/0.89 inference(transitivity,[status(thm)],[117, 107])).
% 0.70/0.89 tff(119,plain,
% 0.70/0.89 (s_e(Xa1!1, Xc!2, Xa1!1, s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) <=> s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa1!1, Xc1!0)),
% 0.70/0.89 inference(monotonicity,[status(thm)],[118, 105])).
% 0.70/0.89 tff(120,plain,
% 0.70/0.89 (s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa1!1, Xc1!0) <=> s_e(Xa1!1, Xc!2, Xa1!1, s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))),
% 0.70/0.89 inference(symmetry,[status(thm)],[119])).
% 0.70/0.89 tff(121,plain,
% 0.70/0.89 ((~![Xa: $i, Xb: $i, Xc: $i] : (~((~((~s_r(Xa, Xb, Xc)) | s_e(Xa, Xc, Xa, s(Xb, Xc)))) | (~(s_r(Xa, Xb, Xc) | (~s_e(Xa, Xc, Xa, s(Xb, Xc)))))))) | (~((~((~s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)) | s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0)))) | (~(s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0) | (~s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0)))))))),
% 0.70/0.89 inference(quant_inst,[status(thm)],[])).
% 0.70/0.89 tff(122,plain,
% 0.70/0.89 (~((~((~s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)) | s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0)))) | (~(s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0) | (~s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))))))),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[121, 94])).
% 0.70/0.89 tff(123,plain,
% 0.70/0.89 (((~((~s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)) | s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0)))) | (~(s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0) | (~s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0)))))) | ((~s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)) | s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0)))),
% 0.70/0.89 inference(tautology,[status(thm)],[])).
% 0.70/0.89 tff(124,plain,
% 0.70/0.89 ((~s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)) | s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[123, 122])).
% 0.70/0.89 tff(125,plain,
% 0.70/0.89 (s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)),
% 0.70/0.89 inference(or_elim,[status(thm)],[10])).
% 0.70/0.89 tff(126,plain,
% 0.70/0.89 ((~((~s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)) | s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0)))) | (~s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)) | s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))),
% 0.70/0.89 inference(tautology,[status(thm)],[])).
% 0.70/0.89 tff(127,plain,
% 0.70/0.89 ((~((~s_r(Xa1!1, midpoint(Xc!2, Xc1!0), Xc1!0)) | s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0)))) | s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[126, 125])).
% 0.70/0.89 tff(128,plain,
% 0.70/0.89 (s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[127, 124])).
% 0.70/0.89 tff(129,plain,
% 0.70/0.89 (^[Xa: $i, Xb: $i, Xc: $i, Xd: $i] : refl(((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb)) <=> ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb)))),
% 0.70/0.89 inference(bind,[status(th)],[])).
% 0.70/0.89 tff(130,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb)) <=> ![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))),
% 0.70/0.89 inference(quant_intro,[status(thm)],[129])).
% 0.70/0.89 tff(131,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb)) <=> ![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))),
% 0.70/0.89 inference(rewrite,[status(thm)],[])).
% 0.70/0.89 tff(132,axiom,(![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','aSatz2_2')).
% 0.70/0.89 tff(133,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[132, 131])).
% 0.70/0.89 tff(134,plain,(
% 0.70/0.89 ![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))),
% 0.70/0.89 inference(skolemize,[status(sab)],[133])).
% 0.70/0.89 tff(135,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[134, 130])).
% 0.70/0.89 tff(136,plain,
% 0.70/0.89 (((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))) | ((~s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) | s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa1!1, Xc1!0))) <=> ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))) | (~s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) | s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa1!1, Xc1!0))),
% 0.70/0.89 inference(rewrite,[status(thm)],[])).
% 0.70/0.89 tff(137,plain,
% 0.70/0.89 ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))) | ((~s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) | s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa1!1, Xc1!0))),
% 0.70/0.89 inference(quant_inst,[status(thm)],[])).
% 0.70/0.89 tff(138,plain,
% 0.70/0.89 ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))) | (~s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) | s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa1!1, Xc1!0)),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[137, 136])).
% 0.70/0.89 tff(139,plain,
% 0.70/0.89 (s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa1!1, Xc1!0)),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[138, 135, 128])).
% 0.70/0.89 tff(140,plain,
% 0.70/0.89 (s_e(Xa1!1, Xc!2, Xa1!1, s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[139, 120])).
% 0.70/0.89 tff(141,plain,
% 0.70/0.89 (s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[140, 100])).
% 0.70/0.89 tff(142,plain,
% 0.70/0.89 ((~(s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2) | (~s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))))) | s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2) | (~s_e(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), s(isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))),
% 0.70/0.89 inference(tautology,[status(thm)],[])).
% 0.70/0.89 tff(143,plain,
% 0.70/0.89 (s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[142, 141, 98])).
% 0.70/0.89 tff(144,plain,
% 0.70/0.89 (s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2) <=> s_e(Xa!3, Xc!2, Xa1!1, Xc!2)),
% 0.70/0.89 inference(monotonicity,[status(thm)],[81])).
% 0.70/0.89 tff(145,plain,
% 0.70/0.89 (s_e(Xa!3, Xc!2, Xa1!1, Xc!2) <=> s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2)),
% 0.70/0.89 inference(symmetry,[status(thm)],[144])).
% 0.70/0.89 tff(146,plain,
% 0.70/0.89 ((~s_e(Xa!3, Xc!2, Xa1!1, Xc!2)) <=> (~s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2))),
% 0.70/0.89 inference(monotonicity,[status(thm)],[145])).
% 0.70/0.89 tff(147,plain,
% 0.70/0.89 (s(midpoint(Xc!2, Xc1!0), Xc1!0) = Xc!2),
% 0.70/0.89 inference(transitivity,[status(thm)],[106, 116])).
% 0.70/0.89 tff(148,plain,
% 0.70/0.89 (s_e(Xa!3, Xc!2, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0)) <=> s_e(Xa!3, Xc!2, Xa1!1, Xc!2)),
% 0.70/0.89 inference(monotonicity,[status(thm)],[147])).
% 0.70/0.89 tff(149,plain,
% 0.70/0.89 ((~s_e(Xa!3, Xc!2, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) <=> (~s_e(Xa!3, Xc!2, Xa1!1, Xc!2))),
% 0.70/0.89 inference(monotonicity,[status(thm)],[148])).
% 0.70/0.89 tff(150,plain,
% 0.70/0.89 (~s_e(Xa!3, Xc!2, Xa1!1, Xc1!0)),
% 0.70/0.89 inference(or_elim,[status(thm)],[10])).
% 0.70/0.89 tff(151,plain,
% 0.70/0.89 (((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))) | ((~s_e(Xa1!1, Xc1!0, Xa!3, Xc!2)) | s_e(Xa!3, Xc!2, Xa1!1, Xc1!0))) <=> ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))) | (~s_e(Xa1!1, Xc1!0, Xa!3, Xc!2)) | s_e(Xa!3, Xc!2, Xa1!1, Xc1!0))),
% 0.70/0.89 inference(rewrite,[status(thm)],[])).
% 0.70/0.89 tff(152,plain,
% 0.70/0.89 ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))) | ((~s_e(Xa1!1, Xc1!0, Xa!3, Xc!2)) | s_e(Xa!3, Xc!2, Xa1!1, Xc1!0))),
% 0.70/0.89 inference(quant_inst,[status(thm)],[])).
% 0.70/0.89 tff(153,plain,
% 0.70/0.89 ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))) | (~s_e(Xa1!1, Xc1!0, Xa!3, Xc!2)) | s_e(Xa!3, Xc!2, Xa1!1, Xc1!0)),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[152, 151])).
% 0.70/0.89 tff(154,plain,
% 0.70/0.89 (~s_e(Xa1!1, Xc1!0, Xa!3, Xc!2)),
% 0.70/0.89 inference(unit_resolution,[status(thm)],[153, 135, 150])).
% 0.70/0.89 tff(155,plain,
% 0.70/0.89 (^[Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : refl((s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf))) <=> (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf))))),
% 0.70/0.89 inference(bind,[status(th)],[])).
% 0.70/0.89 tff(156,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf))) <=> ![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))),
% 0.70/0.89 inference(quant_intro,[status(thm)],[155])).
% 0.70/0.89 tff(157,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf))) <=> ![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))),
% 0.70/0.89 inference(rewrite,[status(thm)],[])).
% 0.70/0.89 tff(158,plain,
% 0.70/0.89 (^[Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : trans(monotonicity(rewrite(((~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf))) <=> ((~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))), ((((~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf))) | s_e(Xa, Xb, Xe, Xf)) <=> (((~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf))) | s_e(Xa, Xb, Xe, Xf)))), rewrite((((~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf))) | s_e(Xa, Xb, Xe, Xf)) <=> (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))), ((((~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf))) | s_e(Xa, Xb, Xe, Xf)) <=> (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))))),
% 0.70/0.89 inference(bind,[status(th)],[])).
% 0.70/0.89 tff(159,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (((~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf))) | s_e(Xa, Xb, Xe, Xf)) <=> ![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))),
% 0.70/0.89 inference(quant_intro,[status(thm)],[158])).
% 0.70/0.89 tff(160,axiom,(![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (((~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf))) | s_e(Xa, Xb, Xe, Xf))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','aSatz2_3')).
% 0.70/0.89 tff(161,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[160, 159])).
% 0.70/0.89 tff(162,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[161, 157])).
% 0.70/0.89 tff(163,plain,(
% 0.70/0.89 ![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))),
% 0.70/0.89 inference(skolemize,[status(sab)],[162])).
% 0.70/0.89 tff(164,plain,
% 0.70/0.89 (![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))),
% 0.70/0.89 inference(modus_ponens,[status(thm)],[163, 156])).
% 0.70/0.89 tff(165,plain,
% 0.70/0.89 (((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))) | (s_e(Xa1!1, Xc1!0, Xa!3, Xc!2) | (~s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) | (~s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa!3, Xc!2)))) <=> ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))) | s_e(Xa1!1, Xc1!0, Xa!3, Xc!2) | (~s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) | (~s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa!3, Xc!2)))),
% 0.70/0.89 inference(rewrite,[status(thm)],[])).
% 0.70/0.89 tff(166,plain,
% 0.70/0.89 ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))) | (s_e(Xa1!1, Xc1!0, Xa!3, Xc!2) | (~s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) | (~s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa!3, Xc!2)))),
% 0.70/0.90 inference(quant_inst,[status(thm)],[])).
% 0.70/0.90 tff(167,plain,
% 0.70/0.90 ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i, Xe: $i, Xf: $i] : (s_e(Xa, Xb, Xe, Xf) | (~s_e(Xa, Xb, Xc, Xd)) | (~s_e(Xc, Xd, Xe, Xf)))) | s_e(Xa1!1, Xc1!0, Xa!3, Xc!2) | (~s_e(Xa1!1, Xc1!0, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) | (~s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa!3, Xc!2))),
% 0.70/0.90 inference(modus_ponens,[status(thm)],[166, 165])).
% 0.70/0.90 tff(168,plain,
% 0.70/0.90 (~s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa!3, Xc!2)),
% 0.70/0.90 inference(unit_resolution,[status(thm)],[167, 164, 154, 128])).
% 0.70/0.90 tff(169,plain,
% 0.70/0.90 (((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))) | ((~s_e(Xa!3, Xc!2, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) | s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa!3, Xc!2))) <=> ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))) | (~s_e(Xa!3, Xc!2, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) | s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa!3, Xc!2))),
% 0.70/0.90 inference(rewrite,[status(thm)],[])).
% 0.70/0.90 tff(170,plain,
% 0.70/0.90 ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))) | ((~s_e(Xa!3, Xc!2, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) | s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa!3, Xc!2))),
% 0.70/0.90 inference(quant_inst,[status(thm)],[])).
% 0.70/0.90 tff(171,plain,
% 0.70/0.90 ((~![Xa: $i, Xb: $i, Xc: $i, Xd: $i] : ((~s_e(Xa, Xb, Xc, Xd)) | s_e(Xc, Xd, Xa, Xb))) | (~s_e(Xa!3, Xc!2, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))) | s_e(Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0), Xa!3, Xc!2)),
% 0.70/0.90 inference(modus_ponens,[status(thm)],[170, 169])).
% 0.70/0.90 tff(172,plain,
% 0.70/0.90 (~s_e(Xa!3, Xc!2, Xa1!1, s(midpoint(Xc!2, Xc1!0), Xc1!0))),
% 0.70/0.90 inference(unit_resolution,[status(thm)],[171, 135, 168])).
% 0.70/0.90 tff(173,plain,
% 0.70/0.90 (~s_e(Xa!3, Xc!2, Xa1!1, Xc!2)),
% 0.70/0.90 inference(modus_ponens,[status(thm)],[172, 149])).
% 0.70/0.90 tff(174,plain,
% 0.70/0.90 (~s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2)),
% 0.70/0.90 inference(modus_ponens,[status(thm)],[173, 146])).
% 0.70/0.90 tff(175,plain,
% 0.70/0.90 (^[Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : refl(((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb))) <=> ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb))))),
% 0.70/0.90 inference(bind,[status(th)],[])).
% 0.70/0.90 tff(176,plain,
% 0.70/0.90 (![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb))) <=> ![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))),
% 0.70/0.90 inference(quant_intro,[status(thm)],[175])).
% 0.70/0.90 tff(177,plain,
% 0.70/0.90 (![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb))) <=> ![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))),
% 0.70/0.90 inference(rewrite,[status(thm)],[])).
% 0.70/0.90 tff(178,plain,
% 0.70/0.90 (^[Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : trans(monotonicity(trans(monotonicity(rewrite(((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc))) <=> ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)))), ((((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc))) | (~s_e(Xa, Xb, Xa1, Xb))) <=> (((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc))) | (~s_e(Xa, Xb, Xa1, Xb))))), rewrite((((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc))) | (~s_e(Xa, Xb, Xa1, Xb))) <=> ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | (~s_e(Xa, Xb, Xa1, Xb)))), ((((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc))) | (~s_e(Xa, Xb, Xa1, Xb))) <=> ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | (~s_e(Xa, Xb, Xa1, Xb))))), (((((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc))) | (~s_e(Xa, Xb, Xa1, Xb))) | s_e(Xa, Xc, Xa1, Xc)) <=> (((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | (~s_e(Xa, Xb, Xa1, Xb))) | s_e(Xa, Xc, Xa1, Xc)))), rewrite((((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | (~s_e(Xa, Xb, Xa1, Xb))) | s_e(Xa, Xc, Xa1, Xc)) <=> ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))), (((((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc))) | (~s_e(Xa, Xb, Xa1, Xb))) | s_e(Xa, Xc, Xa1, Xc)) <=> ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))))),
% 0.70/0.90 inference(bind,[status(th)],[])).
% 0.70/0.90 tff(179,plain,
% 0.70/0.90 (![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc))) | (~s_e(Xa, Xb, Xa1, Xb))) | s_e(Xa, Xc, Xa1, Xc)) <=> ![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))),
% 0.70/0.90 inference(quant_intro,[status(thm)],[178])).
% 0.70/0.90 tff(180,axiom,(![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc))) | (~s_e(Xa, Xb, Xa1, Xb))) | s_e(Xa, Xc, Xa1, Xc))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','aSatz10_12b')).
% 0.70/0.90 tff(181,plain,
% 0.70/0.90 (![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))),
% 0.70/0.90 inference(modus_ponens,[status(thm)],[180, 179])).
% 0.70/0.90 tff(182,plain,
% 0.70/0.90 (![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))),
% 0.70/0.90 inference(modus_ponens,[status(thm)],[181, 177])).
% 0.70/0.90 tff(183,plain,(
% 0.70/0.90 ![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))),
% 0.70/0.90 inference(skolemize,[status(sab)],[182])).
% 0.70/0.90 tff(184,plain,
% 0.70/0.90 (![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))),
% 0.70/0.90 inference(modus_ponens,[status(thm)],[183, 176])).
% 0.70/0.90 tff(185,plain,
% 0.70/0.90 (((~![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))) | (s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2) | (~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | (~s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))) | (~s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))) <=> ((~![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))) | s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2) | (~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | (~s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))) | (~s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))),
% 0.70/0.90 inference(rewrite,[status(thm)],[])).
% 0.70/0.90 tff(186,plain,
% 0.70/0.90 (((~s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | (~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2) | (~s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0))))) <=> (s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2) | (~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | (~s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))) | (~s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))),
% 0.70/0.90 inference(rewrite,[status(thm)],[])).
% 0.70/0.90 tff(187,plain,
% 0.70/0.90 (((~![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))) | ((~s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | (~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2) | (~s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))))) <=> ((~![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))) | (s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2) | (~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | (~s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))) | (~s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))))),
% 0.70/0.91 inference(monotonicity,[status(thm)],[186])).
% 0.70/0.91 tff(188,plain,
% 0.70/0.91 (((~![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))) | ((~s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | (~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2) | (~s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))))) <=> ((~![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))) | s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2) | (~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | (~s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))) | (~s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)))),
% 0.70/0.91 inference(transitivity,[status(thm)],[187, 185])).
% 0.70/0.91 tff(189,plain,
% 0.70/0.91 ((~![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))) | ((~s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | (~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2) | (~s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))))),
% 0.70/0.91 inference(quant_inst,[status(thm)],[])).
% 0.70/0.91 tff(190,plain,
% 0.70/0.91 ((~![Xa: $i, Xb: $i, Xc: $i, Xa1: $i] : ((~s_r(Xa, Xb, Xc)) | (~s_r(Xa1, Xb, Xc)) | s_e(Xa, Xc, Xa1, Xc) | (~s_e(Xa, Xb, Xa1, Xb)))) | s_e(Xa!3, Xc!2, s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), Xc!2) | (~s_r(s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2)) | (~s_e(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), s(isomidpoint(Xa!3, Xa1!1, midpoint(Xc!2, Xc1!0)), Xa!3), isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)))) | (~s_r(Xa!3, isomidpoint(Xc!2, Xc1!0, midpoint(Xc!2, Xc1!0)), Xc!2))),
% 0.70/0.91 inference(modus_ponens,[status(thm)],[189, 188])).
% 0.70/0.91 tff(191,plain,
% 0.70/0.91 ($false),
% 0.70/0.91 inference(unit_resolution,[status(thm)],[190, 184, 174, 143, 84, 53])).
% 0.70/0.91 % SZS output end Proof
% 0.70/0.91 % E exiting
%------------------------------------------------------------------------------