%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : GEO299+1 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n013.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:14 AM UTC 2025
% Result : Theorem 21.51s 21.70s
% Output : Proof 21.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.14 % Problem : GEO299+1 : TPTP v9.0.0. Released v4.1.0.
% 0.07/0.14 % Command : run_E %s %d THM
% 0.13/0.35 % Computer : n013.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 14:46:38 EDT 2025
% 0.13/0.36 % CPUTime :
% 21.51/21.70 % SZS status Theorem
% 21.51/21.70 % SZS output start Proof
% 21.51/21.70 tff(vplus_type, type, (
% 21.51/21.70 vplus: ( $i * $i ) > $i)).
% 21.51/21.70 tff(vf_type, type, (
% 21.51/21.70 vf: ( $i * $i ) > $i)).
% 21.51/21.70 tff(vd1187_type, type, (
% 21.51/21.70 vd1187: $i)).
% 21.51/21.70 tff(vd1201_type, type, (
% 21.51/21.70 vd1201: $i)).
% 21.51/21.70 tff(vd1185_type, type, (
% 21.51/21.70 vd1185: $i)).
% 21.51/21.70 tff(rpoint_type, type, (
% 21.51/21.70 rpoint: $i > $o)).
% 21.51/21.70 tff(vd1186_type, type, (
% 21.51/21.70 vd1186: $i)).
% 21.51/21.70 tff(vd1179_type, type, (
% 21.51/21.70 vd1179: $i)).
% 21.51/21.70 tff(vd1178_type, type, (
% 21.51/21.70 vd1178: $i)).
% 21.51/21.70 tff(vd1180_type, type, (
% 21.51/21.70 vd1180: $i)).
% 21.51/21.70 tff(vangle_type, type, (
% 21.51/21.70 vangle: ( $i * $i * $i ) > $i)).
% 21.51/21.70 tff(rline_type, type, (
% 21.51/21.70 rline: $i > $o)).
% 21.51/21.70 tff(ron_type, type, (
% 21.51/21.70 ron: ( $i * $i ) > $o)).
% 21.51/21.70 tff(rR_type, type, (
% 21.51/21.70 rR: ( $i * $i * $i ) > $o)).
% 21.51/21.70 tff(1,plain,
% 21.51/21.70 (rpoint(vd1185) <=> rpoint(vd1185)),
% 21.51/21.70 inference(rewrite,[status(thm)],[])).
% 21.51/21.70 tff(2,plain,
% 21.51/21.70 (?[Vd1189: $i] : rpoint(vd1185) <=> rpoint(vd1185)),
% 21.51/21.70 inference(elim_unused_vars,[status(thm)],[])).
% 21.51/21.70 tff(3,plain,
% 21.51/21.70 (?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189)) <=> ?[Vd1189: $i] : rpoint(vd1185)),
% 21.51/21.70 inference(destructive_equality_resolution,[status(thm)],[])).
% 21.51/21.70 tff(4,plain,
% 21.51/21.70 (?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189)) <=> rpoint(vd1185)),
% 21.51/21.70 inference(transitivity,[status(thm)],[3, 2])).
% 21.51/21.70 tff(5,axiom,(((((((((((((~?[Vd1195: $i] : (((ron(vd1187, Vd1195) & ron(vd1186, Vd1195)) & ron(vd1185, Vd1195)) & rline(Vd1195))) & (vangle(vd1179, vd1178, vd1180) = vangle(vd1186, vd1185, vd1187))) & (vf(vd1178, vd1180) = vf(vd1185, vd1187))) & (vf(vd1178, vd1179) = vf(vd1185, vd1186))) & ?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191))) & ?[Vd1190: $i] : ((vd1186 = Vd1190) & rpoint(Vd1190))) & ?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189))) & (~(vd1179 = vd1180))) & (~(vd1178 = vd1180))) & (~(vd1178 = vd1179))) & ?[Vd1184: $i] : ((vd1180 = Vd1184) & rpoint(Vd1184))) & ?[Vd1183: $i] : ((vd1179 = Vd1183) & rpoint(Vd1183))) & ?[Vd1182: $i] : ((vd1178 = Vd1182) & rpoint(Vd1182))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))'')).
% 21.51/21.70 tff(6,plain,
% 21.51/21.70 ((((((((((((~?[Vd1195: $i] : (((ron(vd1187, Vd1195) & ron(vd1186, Vd1195)) & ron(vd1185, Vd1195)) & rline(Vd1195))) & (vangle(vd1179, vd1178, vd1180) = vangle(vd1186, vd1185, vd1187))) & (vf(vd1178, vd1180) = vf(vd1185, vd1187))) & (vf(vd1178, vd1179) = vf(vd1185, vd1186))) & ?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191))) & ?[Vd1190: $i] : ((vd1186 = Vd1190) & rpoint(Vd1190))) & ?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189))) & (~(vd1179 = vd1180))) & (~(vd1178 = vd1180))) & (~(vd1178 = vd1179))) & ?[Vd1184: $i] : ((vd1180 = Vd1184) & rpoint(Vd1184))) & ?[Vd1183: $i] : ((vd1179 = Vd1183) & rpoint(Vd1183))),
% 21.51/21.70 inference(and_elim,[status(thm)],[5])).
% 21.51/21.70 tff(7,plain,
% 21.51/21.70 (((((((((((~?[Vd1195: $i] : (((ron(vd1187, Vd1195) & ron(vd1186, Vd1195)) & ron(vd1185, Vd1195)) & rline(Vd1195))) & (vangle(vd1179, vd1178, vd1180) = vangle(vd1186, vd1185, vd1187))) & (vf(vd1178, vd1180) = vf(vd1185, vd1187))) & (vf(vd1178, vd1179) = vf(vd1185, vd1186))) & ?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191))) & ?[Vd1190: $i] : ((vd1186 = Vd1190) & rpoint(Vd1190))) & ?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189))) & (~(vd1179 = vd1180))) & (~(vd1178 = vd1180))) & (~(vd1178 = vd1179))) & ?[Vd1184: $i] : ((vd1180 = Vd1184) & rpoint(Vd1184))),
% 21.51/21.70 inference(and_elim,[status(thm)],[6])).
% 21.51/21.70 tff(8,plain,
% 21.51/21.70 ((((((((((~?[Vd1195: $i] : (((ron(vd1187, Vd1195) & ron(vd1186, Vd1195)) & ron(vd1185, Vd1195)) & rline(Vd1195))) & (vangle(vd1179, vd1178, vd1180) = vangle(vd1186, vd1185, vd1187))) & (vf(vd1178, vd1180) = vf(vd1185, vd1187))) & (vf(vd1178, vd1179) = vf(vd1185, vd1186))) & ?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191))) & ?[Vd1190: $i] : ((vd1186 = Vd1190) & rpoint(Vd1190))) & ?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189))) & (~(vd1179 = vd1180))) & (~(vd1178 = vd1180))) & (~(vd1178 = vd1179))),
% 21.51/21.70 inference(and_elim,[status(thm)],[7])).
% 21.51/21.70 tff(9,plain,
% 21.51/21.70 (((((((((~?[Vd1195: $i] : (((ron(vd1187, Vd1195) & ron(vd1186, Vd1195)) & ron(vd1185, Vd1195)) & rline(Vd1195))) & (vangle(vd1179, vd1178, vd1180) = vangle(vd1186, vd1185, vd1187))) & (vf(vd1178, vd1180) = vf(vd1185, vd1187))) & (vf(vd1178, vd1179) = vf(vd1185, vd1186))) & ?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191))) & ?[Vd1190: $i] : ((vd1186 = Vd1190) & rpoint(Vd1190))) & ?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189))) & (~(vd1179 = vd1180))) & (~(vd1178 = vd1180))),
% 21.51/21.70 inference(and_elim,[status(thm)],[8])).
% 21.51/21.70 tff(10,plain,
% 21.51/21.70 ((((((((~?[Vd1195: $i] : (((ron(vd1187, Vd1195) & ron(vd1186, Vd1195)) & ron(vd1185, Vd1195)) & rline(Vd1195))) & (vangle(vd1179, vd1178, vd1180) = vangle(vd1186, vd1185, vd1187))) & (vf(vd1178, vd1180) = vf(vd1185, vd1187))) & (vf(vd1178, vd1179) = vf(vd1185, vd1186))) & ?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191))) & ?[Vd1190: $i] : ((vd1186 = Vd1190) & rpoint(Vd1190))) & ?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189))) & (~(vd1179 = vd1180))),
% 21.51/21.70 inference(and_elim,[status(thm)],[9])).
% 21.51/21.70 tff(11,plain,
% 21.51/21.70 (((((((~?[Vd1195: $i] : (((ron(vd1187, Vd1195) & ron(vd1186, Vd1195)) & ron(vd1185, Vd1195)) & rline(Vd1195))) & (vangle(vd1179, vd1178, vd1180) = vangle(vd1186, vd1185, vd1187))) & (vf(vd1178, vd1180) = vf(vd1185, vd1187))) & (vf(vd1178, vd1179) = vf(vd1185, vd1186))) & ?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191))) & ?[Vd1190: $i] : ((vd1186 = Vd1190) & rpoint(Vd1190))) & ?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189))),
% 21.51/21.70 inference(and_elim,[status(thm)],[10])).
% 21.51/21.70 tff(12,plain,
% 21.51/21.70 (?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189))),
% 21.51/21.70 inference(and_elim,[status(thm)],[11])).
% 21.51/21.70 tff(13,plain,
% 21.51/21.70 (rpoint(vd1185)),
% 21.51/21.70 inference(modus_ponens,[status(thm)],[12, 4])).
% 21.51/21.70 tff(14,plain,
% 21.51/21.70 (rpoint(vd1185)),
% 21.51/21.70 inference(modus_ponens,[status(thm)],[13, 1])).
% 21.51/21.70 tff(15,plain,
% 21.51/21.70 (rpoint(vd1187) <=> rpoint(vd1187)),
% 21.51/21.70 inference(rewrite,[status(thm)],[])).
% 21.51/21.70 tff(16,plain,
% 21.51/21.70 (?[Vd1191: $i] : rpoint(vd1187) <=> rpoint(vd1187)),
% 21.51/21.70 inference(elim_unused_vars,[status(thm)],[])).
% 21.51/21.70 tff(17,plain,
% 21.51/21.70 (?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191)) <=> ?[Vd1191: $i] : rpoint(vd1187)),
% 21.51/21.70 inference(destructive_equality_resolution,[status(thm)],[])).
% 21.51/21.70 tff(18,plain,
% 21.51/21.70 (?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191)) <=> rpoint(vd1187)),
% 21.51/21.70 inference(transitivity,[status(thm)],[17, 16])).
% 21.51/21.70 tff(19,plain,
% 21.51/21.70 ((((((~?[Vd1195: $i] : (((ron(vd1187, Vd1195) & ron(vd1186, Vd1195)) & ron(vd1185, Vd1195)) & rline(Vd1195))) & (vangle(vd1179, vd1178, vd1180) = vangle(vd1186, vd1185, vd1187))) & (vf(vd1178, vd1180) = vf(vd1185, vd1187))) & (vf(vd1178, vd1179) = vf(vd1185, vd1186))) & ?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191))) & ?[Vd1190: $i] : ((vd1186 = Vd1190) & rpoint(Vd1190))),
% 21.51/21.70 inference(and_elim,[status(thm)],[11])).
% 21.51/21.70 tff(20,plain,
% 21.51/21.70 (((((~?[Vd1195: $i] : (((ron(vd1187, Vd1195) & ron(vd1186, Vd1195)) & ron(vd1185, Vd1195)) & rline(Vd1195))) & (vangle(vd1179, vd1178, vd1180) = vangle(vd1186, vd1185, vd1187))) & (vf(vd1178, vd1180) = vf(vd1185, vd1187))) & (vf(vd1178, vd1179) = vf(vd1185, vd1186))) & ?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191))),
% 21.51/21.70 inference(and_elim,[status(thm)],[19])).
% 21.51/21.70 tff(21,plain,
% 21.51/21.70 (?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191))),
% 21.51/21.70 inference(and_elim,[status(thm)],[20])).
% 21.51/21.70 tff(22,plain,
% 21.51/21.70 (rpoint(vd1187)),
% 21.51/21.70 inference(modus_ponens,[status(thm)],[21, 18])).
% 21.51/21.70 tff(23,plain,
% 21.51/21.70 (rpoint(vd1187)),
% 21.51/21.70 inference(modus_ponens,[status(thm)],[22, 15])).
% 21.51/21.70 tff(24,plain,
% 21.51/21.70 (rpoint(vd1201) <=> rpoint(vd1201)),
% 21.51/21.70 inference(rewrite,[status(thm)],[])).
% 21.51/21.70 tff(25,plain,
% 21.51/21.70 (?[Vd1205: $i] : rpoint(vd1201) <=> rpoint(vd1201)),
% 21.51/21.70 inference(elim_unused_vars,[status(thm)],[])).
% 21.51/21.70 tff(26,plain,
% 21.51/21.70 (?[Vd1205: $i] : ((vd1201 = Vd1205) & rpoint(Vd1205)) <=> ?[Vd1205: $i] : rpoint(vd1201)),
% 21.51/21.70 inference(destructive_equality_resolution,[status(thm)],[])).
% 21.51/21.70 tff(27,plain,
% 21.51/21.70 (?[Vd1205: $i] : ((vd1201 = Vd1205) & rpoint(Vd1205)) <=> rpoint(vd1201)),
% 21.51/21.70 inference(transitivity,[status(thm)],[26, 25])).
% 21.51/21.70 tff(28,axiom,(?[Vd1205: $i] : ((vd1201 = Vd1205) & rpoint(Vd1205))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''qe(s3(plural(271)))'')).
% 21.51/21.70 tff(29,plain,
% 21.51/21.70 (rpoint(vd1201)),
% 21.51/21.70 inference(modus_ponens,[status(thm)],[28, 27])).
% 21.51/21.70 tff(30,plain,
% 21.51/21.70 (rpoint(vd1201)),
% 21.51/21.70 inference(modus_ponens,[status(thm)],[29, 24])).
% 21.51/21.70 tff(31,plain,
% 21.51/21.70 (^[Vd828: $i, Vd829: $i, Vd830: $i] : refl(((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830))) <=> ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830))))),
% 21.51/21.70 inference(bind,[status(th)],[])).
% 21.51/21.70 tff(32,plain,
% 21.51/21.70 (![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830))) <=> ![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))),
% 21.51/21.70 inference(quant_intro,[status(thm)],[31])).
% 21.51/21.70 tff(33,plain,
% 21.51/21.70 (^[Vd828: $i, Vd829: $i, Vd830: $i] : trans(monotonicity(trans(monotonicity(rewrite((rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828)) <=> (~((~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830))))), ((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) <=> (~(~((~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830))))))), rewrite((~(~((~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830))))) <=> ((~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))), ((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) <=> ((~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830))))), (((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830))) <=> (((~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830))))), rewrite((((~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830))) <=> ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))), (((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830))) <=> ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))))),
% 21.51/21.70 inference(bind,[status(th)],[])).
% 21.51/21.70 tff(34,plain,
% 21.51/21.70 (![Vd828: $i, Vd829: $i, Vd830: $i] : ((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830))) <=> ![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))),
% 21.51/21.70 inference(quant_intro,[status(thm)],[33])).
% 21.51/21.70 tff(35,plain,
% 21.51/21.70 (![Vd828: $i, Vd829: $i, Vd830: $i] : ((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830))) <=> ![Vd828: $i, Vd829: $i, Vd830: $i] : ((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)))),
% 21.51/21.70 inference(rewrite,[status(thm)],[])).
% 21.51/21.70 tff(36,plain,
% 21.51/21.70 (^[Vd828: $i, Vd829: $i, Vd830: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((rR(Vd829, Vd828, Vd830) & ?[Vd834: $i] : ((Vd830 = Vd834) & rpoint(Vd834))) <=> (rR(Vd829, Vd828, Vd830) & rpoint(Vd830))), trans(der(?[Vd833: $i] : ((Vd829 = Vd833) & rpoint(Vd833)) <=> ?[Vd833: $i] : rpoint(Vd829)), elim_unused(?[Vd833: $i] : rpoint(Vd829) <=> rpoint(Vd829)), (?[Vd833: $i] : ((Vd829 = Vd833) & rpoint(Vd833)) <=> rpoint(Vd829))), (((rR(Vd829, Vd828, Vd830) & ?[Vd834: $i] : ((Vd830 = Vd834) & rpoint(Vd834))) & ?[Vd833: $i] : ((Vd829 = Vd833) & rpoint(Vd833))) <=> ((rR(Vd829, Vd828, Vd830) & rpoint(Vd830)) & rpoint(Vd829)))), rewrite(((rR(Vd829, Vd828, Vd830) & rpoint(Vd830)) & rpoint(Vd829)) <=> (rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829))), (((rR(Vd829, Vd828, Vd830) & ?[Vd834: $i] : ((Vd830 = Vd834) & rpoint(Vd834))) & ?[Vd833: $i] : ((Vd829 = Vd833) & rpoint(Vd833))) <=> (rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829)))), trans(der(?[Vd832: $i] : ((Vd828 = Vd832) & rpoint(Vd832)) <=> ?[Vd832: $i] : rpoint(Vd828)), elim_unused(?[Vd832: $i] : rpoint(Vd828) <=> rpoint(Vd828)), (?[Vd832: $i] : ((Vd828 = Vd832) & rpoint(Vd832)) <=> rpoint(Vd828))), ((((rR(Vd829, Vd828, Vd830) & ?[Vd834: $i] : ((Vd830 = Vd834) & rpoint(Vd834))) & ?[Vd833: $i] : ((Vd829 = Vd833) & rpoint(Vd833))) & ?[Vd832: $i] : ((Vd828 = Vd832) & rpoint(Vd832))) <=> ((rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829)) & rpoint(Vd828)))), rewrite(((rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829)) & rpoint(Vd828)) <=> (rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))), ((((rR(Vd829, Vd828, Vd830) & ?[Vd834: $i] : ((Vd830 = Vd834) & rpoint(Vd834))) & ?[Vd833: $i] : ((Vd829 = Vd833) & rpoint(Vd833))) & ?[Vd832: $i] : ((Vd828 = Vd832) & rpoint(Vd832))) <=> (rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828)))), (((((rR(Vd829, Vd828, Vd830) & ?[Vd834: $i] : ((Vd830 = Vd834) & rpoint(Vd834))) & ?[Vd833: $i] : ((Vd829 = Vd833) & rpoint(Vd833))) & ?[Vd832: $i] : ((Vd828 = Vd832) & rpoint(Vd832))) => (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830))) <=> ((rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828)) => (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830))))), rewrite(((rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828)) => (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830))) <=> ((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)))), (((((rR(Vd829, Vd828, Vd830) & ?[Vd834: $i] : ((Vd830 = Vd834) & rpoint(Vd834))) & ?[Vd833: $i] : ((Vd829 = Vd833) & rpoint(Vd833))) & ?[Vd832: $i] : ((Vd828 = Vd832) & rpoint(Vd832))) => (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830))) <=> ((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)))))),
% 21.51/21.70 inference(bind,[status(th)],[])).
% 21.51/21.70 tff(37,plain,
% 21.51/21.70 (![Vd828: $i, Vd829: $i, Vd830: $i] : ((((rR(Vd829, Vd828, Vd830) & ?[Vd834: $i] : ((Vd830 = Vd834) & rpoint(Vd834))) & ?[Vd833: $i] : ((Vd829 = Vd833) & rpoint(Vd833))) & ?[Vd832: $i] : ((Vd828 = Vd832) & rpoint(Vd832))) => (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830))) <=> ![Vd828: $i, Vd829: $i, Vd830: $i] : ((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)))),
% 21.51/21.70 inference(quant_intro,[status(thm)],[36])).
% 21.51/21.70 tff(38,axiom,(![Vd828: $i, Vd829: $i, Vd830: $i] : ((((rR(Vd829, Vd828, Vd830) & ?[Vd834: $i] : ((Vd830 = Vd834) & rpoint(Vd834))) & ?[Vd833: $i] : ((Vd829 = Vd833) & rpoint(Vd833))) & ?[Vd832: $i] : ((Vd828 = Vd832) & rpoint(Vd832))) => (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''qu(cond(axiom(180), 0), imp(cond(axiom(180), 0)))'')).
% 21.51/21.70 tff(39,plain,
% 21.51/21.70 (![Vd828: $i, Vd829: $i, Vd830: $i] : ((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)))),
% 21.51/21.70 inference(modus_ponens,[status(thm)],[38, 37])).
% 21.51/21.70 tff(40,plain,
% 21.51/21.70 (![Vd828: $i, Vd829: $i, Vd830: $i] : ((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)))),
% 21.51/21.70 inference(modus_ponens,[status(thm)],[39, 35])).
% 21.51/21.70 tff(41,plain,(
% 21.51/21.70 ![Vd828: $i, Vd829: $i, Vd830: $i] : ((~(rR(Vd829, Vd828, Vd830) & rpoint(Vd830) & rpoint(Vd829) & rpoint(Vd828))) | (vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)))),
% 21.51/21.70 inference(skolemize,[status(sab)],[40])).
% 21.51/21.70 tff(42,plain,
% 21.51/21.70 (![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))),
% 21.51/21.70 inference(modus_ponens,[status(thm)],[41, 34])).
% 21.51/21.70 tff(43,plain,
% 21.51/21.70 (![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))),
% 21.51/21.70 inference(modus_ponens,[status(thm)],[42, 32])).
% 21.51/21.70 tff(44,plain,
% 21.51/21.70 (rR(vd1201, vd1185, vd1187) <=> rR(vd1201, vd1185, vd1187)),
% 21.51/21.70 inference(rewrite,[status(thm)],[])).
% 21.51/21.70 tff(45,axiom,(rR(vd1201, vd1185, vd1187)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''holds(323, 1254, 0)'')).
% 21.51/21.70 tff(46,plain,
% 21.51/21.70 (rR(vd1201, vd1185, vd1187)),
% 21.51/21.70 inference(modus_ponens,[status(thm)],[45, 44])).
% 21.51/21.70 tff(47,plain,
% 21.51/21.70 (((~![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))) | ((~rpoint(vd1201)) | (~rpoint(vd1185)) | (~rpoint(vd1187)) | (~rR(vd1201, vd1185, vd1187)) | (vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)) = vf(vd1185, vd1187)))) <=> ((~![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))) | (~rpoint(vd1201)) | (~rpoint(vd1185)) | (~rpoint(vd1187)) | (~rR(vd1201, vd1185, vd1187)) | (vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)) = vf(vd1185, vd1187)))),
% 21.51/21.70 inference(rewrite,[status(thm)],[])).
% 21.51/21.70 tff(48,plain,
% 21.51/21.70 (((vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)) = vf(vd1185, vd1187)) | (~rpoint(vd1185)) | (~rpoint(vd1201)) | (~rpoint(vd1187)) | (~rR(vd1201, vd1185, vd1187))) <=> ((~rpoint(vd1201)) | (~rpoint(vd1185)) | (~rpoint(vd1187)) | (~rR(vd1201, vd1185, vd1187)) | (vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)) = vf(vd1185, vd1187)))),
% 21.51/21.70 inference(rewrite,[status(thm)],[])).
% 21.51/21.70 tff(49,plain,
% 21.51/21.70 (((~![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))) | ((vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)) = vf(vd1185, vd1187)) | (~rpoint(vd1185)) | (~rpoint(vd1201)) | (~rpoint(vd1187)) | (~rR(vd1201, vd1185, vd1187)))) <=> ((~![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))) | ((~rpoint(vd1201)) | (~rpoint(vd1185)) | (~rpoint(vd1187)) | (~rR(vd1201, vd1185, vd1187)) | (vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)) = vf(vd1185, vd1187))))),
% 21.51/21.70 inference(monotonicity,[status(thm)],[48])).
% 21.51/21.70 tff(50,plain,
% 21.51/21.70 (((~![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))) | ((vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)) = vf(vd1185, vd1187)) | (~rpoint(vd1185)) | (~rpoint(vd1201)) | (~rpoint(vd1187)) | (~rR(vd1201, vd1185, vd1187)))) <=> ((~![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))) | (~rpoint(vd1201)) | (~rpoint(vd1185)) | (~rpoint(vd1187)) | (~rR(vd1201, vd1185, vd1187)) | (vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)) = vf(vd1185, vd1187)))),
% 21.63/21.82 inference(transitivity,[status(thm)],[49, 47])).
% 21.63/21.82 tff(51,plain,
% 21.63/21.82 ((~![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))) | ((vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)) = vf(vd1185, vd1187)) | (~rpoint(vd1185)) | (~rpoint(vd1201)) | (~rpoint(vd1187)) | (~rR(vd1201, vd1185, vd1187)))),
% 21.63/21.82 inference(quant_inst,[status(thm)],[])).
% 21.63/21.82 tff(52,plain,
% 21.63/21.82 ((~![Vd828: $i, Vd829: $i, Vd830: $i] : ((vplus(vf(Vd828, Vd829), vf(Vd829, Vd830)) = vf(Vd828, Vd830)) | (~rpoint(Vd828)) | (~rpoint(Vd829)) | (~rpoint(Vd830)) | (~rR(Vd829, Vd828, Vd830)))) | (~rpoint(vd1201)) | (~rpoint(vd1185)) | (~rpoint(vd1187)) | (~rR(vd1201, vd1185, vd1187)) | (vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)) = vf(vd1185, vd1187))),
% 21.63/21.82 inference(modus_ponens,[status(thm)],[51, 50])).
% 21.63/21.82 tff(53,plain,
% 21.63/21.82 (vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)) = vf(vd1185, vd1187)),
% 21.63/21.82 inference(unit_resolution,[status(thm)],[52, 46, 43, 30, 23, 14])).
% 21.63/21.82 tff(54,plain,
% 21.63/21.82 (vf(vd1185, vd1187) = vplus(vf(vd1185, vd1201), vf(vd1201, vd1187))),
% 21.63/21.82 inference(symmetry,[status(thm)],[53])).
% 21.63/21.82 tff(55,plain,
% 21.63/21.82 ((~(vf(vd1185, vd1187) = vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)))) <=> (~(vf(vd1185, vd1187) = vplus(vf(vd1185, vd1201), vf(vd1201, vd1187))))),
% 21.63/21.82 inference(rewrite,[status(thm)],[])).
% 21.63/21.82 tff(56,axiom,(~(vf(vd1185, vd1187) = vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''holds(324, 1255, 0)'')).
% 21.63/21.82 tff(57,plain,
% 21.63/21.82 (~(vf(vd1185, vd1187) = vplus(vf(vd1185, vd1201), vf(vd1201, vd1187)))),
% 21.63/21.82 inference(modus_ponens,[status(thm)],[56, 55])).
% 21.63/21.82 tff(58,plain,
% 21.63/21.82 ($false),
% 21.63/21.82 inference(unit_resolution,[status(thm)],[57, 54])).
% 21.63/21.82 % SZS output end Proof
% 21.63/21.82 % E exiting
%------------------------------------------------------------------------------