%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : GEO300+1 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n007.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 20.78s 20.95s
% Output : Proof 20.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.11 % Problem : GEO300+1 : TPTP v9.0.0. Released v4.1.0.
% 0.09/0.11 % Command : run_E %s %d THM
% 0.12/0.32 % Computer : n007.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Thu Jun 19 14:47:49 EDT 2025
% 0.12/0.33 % CPUTime :
% 20.78/20.95 % SZS status Theorem
% 20.78/20.95 % SZS output start Proof
% 20.78/20.95 tff(vplus_type, type, (
% 20.78/20.95 vplus: ( $i * $i ) > $i)).
% 20.78/20.95 tff(vf_type, type, (
% 20.78/20.95 vf: ( $i * $i ) > $i)).
% 20.78/20.95 tff(vd1201_type, type, (
% 20.78/20.95 vd1201: $i)).
% 20.78/20.95 tff(vd1187_type, type, (
% 20.78/20.95 vd1187: $i)).
% 20.78/20.95 tff(vd1185_type, type, (
% 20.78/20.95 vd1185: $i)).
% 20.78/20.95 tff(rpoint_type, type, (
% 20.78/20.95 rpoint: $i > $o)).
% 20.78/20.95 tff(vd1186_type, type, (
% 20.78/20.95 vd1186: $i)).
% 20.78/20.95 tff(vd1179_type, type, (
% 20.78/20.95 vd1179: $i)).
% 20.78/20.95 tff(vd1178_type, type, (
% 20.78/20.95 vd1178: $i)).
% 20.78/20.95 tff(vd1180_type, type, (
% 20.78/20.95 vd1180: $i)).
% 20.78/20.95 tff(vangle_type, type, (
% 20.78/20.95 vangle: ( $i * $i * $i ) > $i)).
% 20.78/20.95 tff(rline_type, type, (
% 20.78/20.95 rline: $i > $o)).
% 20.78/20.95 tff(ron_type, type, (
% 20.78/20.95 ron: ( $i * $i ) > $o)).
% 20.78/20.95 tff(rR_type, type, (
% 20.78/20.95 rR: ( $i * $i * $i ) > $o)).
% 20.78/20.95 tff(1,plain,
% 20.78/20.95 (rpoint(vd1185) <=> rpoint(vd1185)),
% 20.78/20.95 inference(rewrite,[status(thm)],[])).
% 20.78/20.95 tff(2,plain,
% 20.78/20.95 (?[Vd1189: $i] : rpoint(vd1185) <=> rpoint(vd1185)),
% 20.78/20.95 inference(elim_unused_vars,[status(thm)],[])).
% 20.78/20.95 tff(3,plain,
% 20.78/20.95 (?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189)) <=> ?[Vd1189: $i] : rpoint(vd1185)),
% 20.78/20.95 inference(destructive_equality_resolution,[status(thm)],[])).
% 20.78/20.95 tff(4,plain,
% 20.78/20.95 (?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189)) <=> rpoint(vd1185)),
% 20.78/20.95 inference(transitivity,[status(thm)],[3, 2])).
% 20.78/20.95 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/sandbox2/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)))))))))))))))'')).
% 20.78/20.95 tff(6,plain,
% 20.78/20.95 ((((((((((((~?[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))),
% 20.78/20.95 inference(and_elim,[status(thm)],[5])).
% 20.78/20.95 tff(7,plain,
% 20.78/20.95 (((((((((((~?[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))),
% 20.78/20.95 inference(and_elim,[status(thm)],[6])).
% 20.78/20.95 tff(8,plain,
% 20.78/20.95 ((((((((((~?[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))),
% 20.78/20.95 inference(and_elim,[status(thm)],[7])).
% 20.78/20.95 tff(9,plain,
% 20.78/20.95 (((((((((~?[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))),
% 20.78/20.95 inference(and_elim,[status(thm)],[8])).
% 20.78/20.95 tff(10,plain,
% 20.78/20.95 ((((((((~?[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))),
% 20.78/20.95 inference(and_elim,[status(thm)],[9])).
% 20.78/20.95 tff(11,plain,
% 20.78/20.95 (((((((~?[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))),
% 20.78/20.95 inference(and_elim,[status(thm)],[10])).
% 20.78/20.95 tff(12,plain,
% 20.78/20.95 (?[Vd1189: $i] : ((vd1185 = Vd1189) & rpoint(Vd1189))),
% 20.78/20.95 inference(and_elim,[status(thm)],[11])).
% 20.78/20.95 tff(13,plain,
% 20.78/20.95 (rpoint(vd1185)),
% 20.78/20.95 inference(modus_ponens,[status(thm)],[12, 4])).
% 20.78/20.95 tff(14,plain,
% 20.78/20.95 (rpoint(vd1185)),
% 20.78/20.95 inference(modus_ponens,[status(thm)],[13, 1])).
% 20.78/20.95 tff(15,plain,
% 20.78/20.95 (rpoint(vd1187) <=> rpoint(vd1187)),
% 20.78/20.95 inference(rewrite,[status(thm)],[])).
% 20.78/20.95 tff(16,plain,
% 20.78/20.95 (?[Vd1191: $i] : rpoint(vd1187) <=> rpoint(vd1187)),
% 20.78/20.95 inference(elim_unused_vars,[status(thm)],[])).
% 20.78/20.95 tff(17,plain,
% 20.78/20.95 (?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191)) <=> ?[Vd1191: $i] : rpoint(vd1187)),
% 20.78/20.95 inference(destructive_equality_resolution,[status(thm)],[])).
% 20.78/20.95 tff(18,plain,
% 20.78/20.95 (?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191)) <=> rpoint(vd1187)),
% 20.78/20.95 inference(transitivity,[status(thm)],[17, 16])).
% 20.78/20.95 tff(19,plain,
% 20.78/20.95 ((((((~?[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))),
% 20.78/20.95 inference(and_elim,[status(thm)],[11])).
% 20.78/20.95 tff(20,plain,
% 20.78/20.95 (((((~?[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))),
% 20.78/20.95 inference(and_elim,[status(thm)],[19])).
% 20.78/20.95 tff(21,plain,
% 20.78/20.95 (?[Vd1191: $i] : ((vd1187 = Vd1191) & rpoint(Vd1191))),
% 20.78/20.95 inference(and_elim,[status(thm)],[20])).
% 20.78/20.95 tff(22,plain,
% 20.78/20.95 (rpoint(vd1187)),
% 20.78/20.95 inference(modus_ponens,[status(thm)],[21, 18])).
% 20.78/20.95 tff(23,plain,
% 20.78/20.95 (rpoint(vd1187)),
% 20.78/20.95 inference(modus_ponens,[status(thm)],[22, 15])).
% 20.78/20.95 tff(24,plain,
% 20.78/20.95 (rpoint(vd1201) <=> rpoint(vd1201)),
% 20.78/20.95 inference(rewrite,[status(thm)],[])).
% 20.78/20.95 tff(25,plain,
% 20.78/20.95 (?[Vd1205: $i] : rpoint(vd1201) <=> rpoint(vd1201)),
% 20.78/20.95 inference(elim_unused_vars,[status(thm)],[])).
% 20.78/20.95 tff(26,plain,
% 20.78/20.95 (?[Vd1205: $i] : ((vd1201 = Vd1205) & rpoint(Vd1205)) <=> ?[Vd1205: $i] : rpoint(vd1201)),
% 20.78/20.95 inference(destructive_equality_resolution,[status(thm)],[])).
% 20.78/20.95 tff(27,plain,
% 20.78/20.95 (?[Vd1205: $i] : ((vd1201 = Vd1205) & rpoint(Vd1205)) <=> rpoint(vd1201)),
% 20.78/20.95 inference(transitivity,[status(thm)],[26, 25])).
% 20.78/20.95 tff(28,axiom,(?[Vd1205: $i] : ((vd1201 = Vd1205) & rpoint(Vd1205))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''qe(s3(plural(271)))'')).
% 20.78/20.95 tff(29,plain,
% 20.78/20.95 (rpoint(vd1201)),
% 20.78/20.95 inference(modus_ponens,[status(thm)],[28, 27])).
% 20.78/20.95 tff(30,plain,
% 20.78/20.95 (rpoint(vd1201)),
% 20.78/20.95 inference(modus_ponens,[status(thm)],[29, 24])).
% 20.78/20.95 tff(31,plain,
% 20.78/20.95 (^[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))))),
% 20.78/20.95 inference(bind,[status(th)],[])).
% 20.78/20.95 tff(32,plain,
% 20.78/20.95 (![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)))),
% 20.78/20.95 inference(quant_intro,[status(thm)],[31])).
% 20.78/20.95 tff(33,plain,
% 20.78/20.95 (^[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)))))),
% 20.78/20.95 inference(bind,[status(th)],[])).
% 20.78/20.95 tff(34,plain,
% 20.78/20.95 (![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)))),
% 20.78/20.95 inference(quant_intro,[status(thm)],[33])).
% 20.78/20.95 tff(35,plain,
% 20.78/20.95 (![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)))),
% 20.78/20.96 inference(rewrite,[status(thm)],[])).
% 20.78/20.96 tff(36,plain,
% 20.78/20.96 (^[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)))))),
% 20.78/20.96 inference(bind,[status(th)],[])).
% 20.78/20.96 tff(37,plain,
% 20.78/20.96 (![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)))),
% 20.78/20.96 inference(quant_intro,[status(thm)],[36])).
% 20.78/20.96 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/sandbox2/benchmark/theBenchmark.p',''qu(cond(axiom(180), 0), imp(cond(axiom(180), 0)))'')).
% 20.78/20.96 tff(39,plain,
% 20.78/20.96 (![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)))),
% 20.78/20.96 inference(modus_ponens,[status(thm)],[38, 37])).
% 20.78/20.96 tff(40,plain,
% 20.78/20.96 (![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)))),
% 20.78/20.96 inference(modus_ponens,[status(thm)],[39, 35])).
% 20.78/20.96 tff(41,plain,(
% 20.78/20.96 ![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)))),
% 20.78/20.96 inference(skolemize,[status(sab)],[40])).
% 20.78/20.96 tff(42,plain,
% 20.78/20.96 (![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)))),
% 20.78/20.96 inference(modus_ponens,[status(thm)],[41, 34])).
% 20.78/20.96 tff(43,plain,
% 20.78/20.96 (![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)))),
% 20.78/20.96 inference(modus_ponens,[status(thm)],[42, 32])).
% 20.78/20.96 tff(44,plain,
% 20.78/20.96 (rR(vd1187, vd1185, vd1201) <=> rR(vd1187, vd1185, vd1201)),
% 20.78/20.96 inference(rewrite,[status(thm)],[])).
% 20.78/20.96 tff(45,axiom,(rR(vd1187, vd1185, vd1201)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''holds(330, 1259, 0)'')).
% 20.78/20.96 tff(46,plain,
% 20.78/20.96 (rR(vd1187, vd1185, vd1201)),
% 20.78/20.96 inference(modus_ponens,[status(thm)],[45, 44])).
% 20.78/20.96 tff(47,plain,
% 20.78/20.96 (((~![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(vd1185)) | (~rpoint(vd1201)) | (~rpoint(vd1187)) | (~rR(vd1187, vd1185, vd1201)) | (vplus(vf(vd1185, vd1187), vf(vd1187, vd1201)) = vf(vd1185, vd1201)))) <=> ((~![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(vd1185)) | (~rpoint(vd1201)) | (~rpoint(vd1187)) | (~rR(vd1187, vd1185, vd1201)) | (vplus(vf(vd1185, vd1187), vf(vd1187, vd1201)) = vf(vd1185, vd1201)))),
% 20.78/20.96 inference(rewrite,[status(thm)],[])).
% 20.78/20.96 tff(48,plain,
% 20.78/20.96 (((vplus(vf(vd1185, vd1187), vf(vd1187, vd1201)) = vf(vd1185, vd1201)) | (~rpoint(vd1185)) | (~rpoint(vd1187)) | (~rpoint(vd1201)) | (~rR(vd1187, vd1185, vd1201))) <=> ((~rpoint(vd1185)) | (~rpoint(vd1201)) | (~rpoint(vd1187)) | (~rR(vd1187, vd1185, vd1201)) | (vplus(vf(vd1185, vd1187), vf(vd1187, vd1201)) = vf(vd1185, vd1201)))),
% 20.78/20.96 inference(rewrite,[status(thm)],[])).
% 20.78/20.96 tff(49,plain,
% 20.78/20.96 (((~![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, vd1187), vf(vd1187, vd1201)) = vf(vd1185, vd1201)) | (~rpoint(vd1185)) | (~rpoint(vd1187)) | (~rpoint(vd1201)) | (~rR(vd1187, vd1185, vd1201)))) <=> ((~![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(vd1185)) | (~rpoint(vd1201)) | (~rpoint(vd1187)) | (~rR(vd1187, vd1185, vd1201)) | (vplus(vf(vd1185, vd1187), vf(vd1187, vd1201)) = vf(vd1185, vd1201))))),
% 20.78/20.96 inference(monotonicity,[status(thm)],[48])).
% 20.78/20.96 tff(50,plain,
% 20.78/20.96 (((~![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, vd1187), vf(vd1187, vd1201)) = vf(vd1185, vd1201)) | (~rpoint(vd1185)) | (~rpoint(vd1187)) | (~rpoint(vd1201)) | (~rR(vd1187, vd1185, vd1201)))) <=> ((~![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(vd1185)) | (~rpoint(vd1201)) | (~rpoint(vd1187)) | (~rR(vd1187, vd1185, vd1201)) | (vplus(vf(vd1185, vd1187), vf(vd1187, vd1201)) = vf(vd1185, vd1201)))),
% 20.86/21.06 inference(transitivity,[status(thm)],[49, 47])).
% 20.86/21.06 tff(51,plain,
% 20.86/21.06 ((~![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, vd1187), vf(vd1187, vd1201)) = vf(vd1185, vd1201)) | (~rpoint(vd1185)) | (~rpoint(vd1187)) | (~rpoint(vd1201)) | (~rR(vd1187, vd1185, vd1201)))),
% 20.86/21.06 inference(quant_inst,[status(thm)],[])).
% 20.86/21.06 tff(52,plain,
% 20.86/21.06 ((~![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(vd1185)) | (~rpoint(vd1201)) | (~rpoint(vd1187)) | (~rR(vd1187, vd1185, vd1201)) | (vplus(vf(vd1185, vd1187), vf(vd1187, vd1201)) = vf(vd1185, vd1201))),
% 20.86/21.06 inference(modus_ponens,[status(thm)],[51, 50])).
% 20.86/21.06 tff(53,plain,
% 20.86/21.06 (vplus(vf(vd1185, vd1187), vf(vd1187, vd1201)) = vf(vd1185, vd1201)),
% 20.86/21.06 inference(unit_resolution,[status(thm)],[52, 46, 43, 30, 23, 14])).
% 20.86/21.06 tff(54,plain,
% 20.86/21.06 (vf(vd1185, vd1201) = vplus(vf(vd1185, vd1187), vf(vd1187, vd1201))),
% 20.86/21.06 inference(symmetry,[status(thm)],[53])).
% 20.86/21.06 tff(55,plain,
% 20.86/21.06 ((~(vf(vd1185, vd1201) = vplus(vf(vd1185, vd1187), vf(vd1187, vd1201)))) <=> (~(vf(vd1185, vd1201) = vplus(vf(vd1185, vd1187), vf(vd1187, vd1201))))),
% 20.86/21.06 inference(rewrite,[status(thm)],[])).
% 20.86/21.06 tff(56,axiom,(~(vf(vd1185, vd1201) = vplus(vf(vd1185, vd1187), vf(vd1187, vd1201)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''holds(331, 1260, 0)'')).
% 20.86/21.06 tff(57,plain,
% 20.86/21.06 (~(vf(vd1185, vd1201) = vplus(vf(vd1185, vd1187), vf(vd1187, vd1201)))),
% 20.86/21.06 inference(modus_ponens,[status(thm)],[56, 55])).
% 20.86/21.06 tff(58,plain,
% 20.86/21.06 ($false),
% 20.86/21.06 inference(unit_resolution,[status(thm)],[57, 54])).
% 20.86/21.06 % SZS output end Proof
% 20.86/21.06 % E exiting
%------------------------------------------------------------------------------