%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : GEO275+1 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n016.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:12 AM UTC 2025
% Result : Theorem 0.21s 0.52s
% Output : Proof 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : GEO275+1 : TPTP v9.0.0. Released v4.1.0.
% 0.11/0.13 % Command : run_E %s %d THM
% 0.13/0.34 % Computer : n016.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu Jun 19 14:44:32 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.21/0.52 % SZS status Theorem
% 0.21/0.52 % SZS output start Proof
% 0.21/0.52 tff(rcenter_type, type, (
% 0.21/0.52 rcenter: ( $i * $i ) > $o)).
% 0.21/0.52 tff(vf_type, type, (
% 0.21/0.52 vf: ( $i * $i ) > $i)).
% 0.21/0.52 tff(ron_type, type, (
% 0.21/0.52 ron: ( $i * $i ) > $o)).
% 0.21/0.52 tff(rpoint_type, type, (
% 0.21/0.52 rpoint: $i > $o)).
% 0.21/0.52 tff(vd1081_type, type, (
% 0.21/0.52 vd1081: $i)).
% 0.21/0.52 tff(vd1095_type, type, (
% 0.21/0.52 vd1095: $i)).
% 0.21/0.52 tff(vd1080_type, type, (
% 0.21/0.52 vd1080: $i)).
% 0.21/0.52 tff(rcircle_type, type, (
% 0.21/0.52 rcircle: $i > $o)).
% 0.21/0.52 tff(tptp_fun_Vdthex_0_type, type, (
% 0.21/0.52 tptp_fun_Vdthex_0: $i)).
% 0.21/0.52 tff(1,plain,
% 0.21/0.52 (^[Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : refl(((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844))) <=> ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844))))),
% 0.21/0.52 inference(bind,[status(th)],[])).
% 0.21/0.52 tff(2,plain,
% 0.21/0.52 (![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844))) <=> ![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))),
% 0.21/0.52 inference(quant_intro,[status(thm)],[1])).
% 0.21/0.52 tff(3,plain,
% 0.21/0.52 (^[Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : trans(monotonicity(trans(monotonicity(rewrite(((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837)) <=> (~((~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844))))), ((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) <=> (~(~((~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844))))))), rewrite((~(~((~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844))))) <=> ((~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))), ((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) <=> ((~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844))))), (((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) | (Vd843 = Vd844)) <=> (((~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844))) | (Vd843 = Vd844)))), rewrite((((~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844))) | (Vd843 = Vd844)) <=> ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))), (((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) | (Vd843 = Vd844)) <=> ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))))),
% 0.21/0.52 inference(bind,[status(th)],[])).
% 0.21/0.52 tff(4,plain,
% 0.21/0.52 (![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) | (Vd843 = Vd844)) <=> ![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))),
% 0.21/0.52 inference(quant_intro,[status(thm)],[3])).
% 0.21/0.52 tff(5,plain,
% 0.21/0.52 (![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) | (Vd843 = Vd844)) <=> ![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) | (Vd843 = Vd844))),
% 0.21/0.52 inference(rewrite,[status(thm)],[])).
% 0.21/0.52 tff(6,plain,
% 0.21/0.52 (^[Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) <=> ((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843))), (((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) <=> (((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)))), rewrite((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) <=> ((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844))), (((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) <=> ((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844)))), ((((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) & rcenter(Vd842, Vd843)) <=> (((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844)) & rcenter(Vd842, Vd843)))), rewrite((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844)) & rcenter(Vd842, Vd843)) <=> ((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843))), ((((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) & rcenter(Vd842, Vd843)) <=> ((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843)))), trans(der(?[Vd841: $i] : ((Vd838 = Vd841) & rpoint(Vd841)) <=> ?[Vd841: $i] : rpoint(Vd838)), elim_unused(?[Vd841: $i] : rpoint(Vd838) <=> rpoint(Vd838)), (?[Vd841: $i] : ((Vd838 = Vd841) & rpoint(Vd841)) <=> rpoint(Vd838))), (((((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) & rcenter(Vd842, Vd843)) & ?[Vd841: $i] : ((Vd838 = Vd841) & rpoint(Vd841))) <=> (((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843)) & rpoint(Vd838)))), rewrite((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843)) & rpoint(Vd838)) <=> ((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838))), (((((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) & rcenter(Vd842, Vd843)) & ?[Vd841: $i] : ((Vd838 = Vd841) & rpoint(Vd841))) <=> ((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838)))), trans(der(?[Vd840: $i] : ((Vd837 = Vd840) & rpoint(Vd840)) <=> ?[Vd840: $i] : rpoint(Vd837)), elim_unused(?[Vd840: $i] : rpoint(Vd837) <=> rpoint(Vd837)), (?[Vd840: $i] : ((Vd837 = Vd840) & rpoint(Vd840)) <=> rpoint(Vd837))), ((((((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) & rcenter(Vd842, Vd843)) & ?[Vd841: $i] : ((Vd838 = Vd841) & rpoint(Vd841))) & ?[Vd840: $i] : ((Vd837 = Vd840) & rpoint(Vd840))) <=> (((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838)) & rpoint(Vd837)))), rewrite((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838)) & rpoint(Vd837)) <=> ((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))), ((((((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) & rcenter(Vd842, Vd843)) & ?[Vd841: $i] : ((Vd838 = Vd841) & rpoint(Vd841))) & ?[Vd840: $i] : ((Vd837 = Vd840) & rpoint(Vd840))) <=> ((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837)))), (((((((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) & rcenter(Vd842, Vd843)) & ?[Vd841: $i] : ((Vd838 = Vd841) & rpoint(Vd841))) & ?[Vd840: $i] : ((Vd837 = Vd840) & rpoint(Vd840))) => (Vd843 = Vd844)) <=> (((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837)) => (Vd843 = Vd844)))), rewrite((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837)) => (Vd843 = Vd844)) <=> ((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) | (Vd843 = Vd844))), (((((((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) & rcenter(Vd842, Vd843)) & ?[Vd841: $i] : ((Vd838 = Vd841) & rpoint(Vd841))) & ?[Vd840: $i] : ((Vd837 = Vd840) & rpoint(Vd840))) => (Vd843 = Vd844)) <=> ((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) | (Vd843 = Vd844))))),
% 0.21/0.52 inference(bind,[status(th)],[])).
% 0.21/0.52 tff(7,plain,
% 0.21/0.52 (![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((((((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) & rcenter(Vd842, Vd843)) & ?[Vd841: $i] : ((Vd838 = Vd841) & rpoint(Vd841))) & ?[Vd840: $i] : ((Vd837 = Vd840) & rpoint(Vd840))) => (Vd843 = Vd844)) <=> ![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) | (Vd843 = Vd844))),
% 0.21/0.52 inference(quant_intro,[status(thm)],[6])).
% 0.21/0.52 tff(8,axiom,(![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((((((((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844)) & ron(Vd837, Vd843)) & rcenter(Vd842, Vd844)) & rcenter(Vd842, Vd843)) & ?[Vd841: $i] : ((Vd838 = Vd841) & rpoint(Vd841))) & ?[Vd840: $i] : ((Vd837 = Vd840) & rpoint(Vd840))) => (Vd843 = Vd844))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))'')).
% 0.21/0.52 tff(9,plain,
% 0.21/0.52 (![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) | (Vd843 = Vd844))),
% 0.21/0.52 inference(modus_ponens,[status(thm)],[8, 7])).
% 0.21/0.52 tff(10,plain,
% 0.21/0.52 (![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) | (Vd843 = Vd844))),
% 0.21/0.52 inference(modus_ponens,[status(thm)],[9, 5])).
% 0.21/0.52 tff(11,plain,(
% 0.21/0.52 ![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((~((vf(Vd842, Vd837) = vf(Vd842, Vd838)) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & rpoint(Vd838) & rpoint(Vd837))) | (Vd843 = Vd844))),
% 0.21/0.52 inference(skolemize,[status(sab)],[10])).
% 0.21/0.52 tff(12,plain,
% 0.21/0.52 (![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))),
% 0.21/0.52 inference(modus_ponens,[status(thm)],[11, 4])).
% 0.21/0.52 tff(13,plain,
% 0.21/0.52 (![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))),
% 0.21/0.52 inference(modus_ponens,[status(thm)],[12, 2])).
% 0.21/0.52 tff(14,plain,
% 0.21/0.52 (rpoint(vd1081) <=> rpoint(vd1081)),
% 0.21/0.52 inference(rewrite,[status(thm)],[])).
% 0.21/0.52 tff(15,plain,
% 0.21/0.52 (?[Vd1084: $i] : rpoint(vd1081) <=> rpoint(vd1081)),
% 0.21/0.52 inference(elim_unused_vars,[status(thm)],[])).
% 0.21/0.52 tff(16,plain,
% 0.21/0.52 (?[Vd1084: $i] : ((vd1081 = Vd1084) & rpoint(Vd1084)) <=> ?[Vd1084: $i] : rpoint(vd1081)),
% 0.21/0.52 inference(destructive_equality_resolution,[status(thm)],[])).
% 0.21/0.52 tff(17,plain,
% 0.21/0.52 (?[Vd1084: $i] : ((vd1081 = Vd1084) & rpoint(Vd1084)) <=> rpoint(vd1081)),
% 0.21/0.52 inference(transitivity,[status(thm)],[16, 15])).
% 0.21/0.52 tff(18,axiom,(?[Vd1084: $i] : ((vd1081 = Vd1084) & rpoint(Vd1084))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''qe(s2(plural(224)))'')).
% 0.21/0.52 tff(19,plain,
% 0.21/0.52 (rpoint(vd1081)),
% 0.21/0.52 inference(modus_ponens,[status(thm)],[18, 17])).
% 0.21/0.52 tff(20,plain,
% 0.21/0.52 (rpoint(vd1081)),
% 0.21/0.52 inference(modus_ponens,[status(thm)],[19, 14])).
% 0.21/0.52 tff(21,plain,
% 0.21/0.52 (rcenter(vd1080, vd1095) <=> rcenter(vd1080, vd1095)),
% 0.21/0.52 inference(rewrite,[status(thm)],[])).
% 0.21/0.52 tff(22,axiom,((ron(vd1081, vd1095) & rcenter(vd1080, vd1095)) & rcircle(vd1095)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''and(pred(comma_conjunct2(the(228)), 0), and(pred(comma_conjunct1(the(228)), 0), pred(the(228), 0)))'')).
% 0.21/0.52 tff(23,plain,
% 0.21/0.52 (ron(vd1081, vd1095) & rcenter(vd1080, vd1095)),
% 0.21/0.52 inference(and_elim,[status(thm)],[22])).
% 0.21/0.52 tff(24,plain,
% 0.21/0.52 (rcenter(vd1080, vd1095)),
% 0.21/0.52 inference(and_elim,[status(thm)],[23])).
% 0.21/0.52 tff(25,plain,
% 0.21/0.52 (rcenter(vd1080, vd1095)),
% 0.21/0.52 inference(modus_ponens,[status(thm)],[24, 21])).
% 0.21/0.52 tff(26,plain,
% 0.21/0.52 (ron(vd1081, vd1095) <=> ron(vd1081, vd1095)),
% 0.21/0.52 inference(rewrite,[status(thm)],[])).
% 0.21/0.52 tff(27,plain,
% 0.21/0.52 (ron(vd1081, vd1095)),
% 0.21/0.52 inference(and_elim,[status(thm)],[23])).
% 0.21/0.52 tff(28,plain,
% 0.21/0.52 (ron(vd1081, vd1095)),
% 0.21/0.52 inference(modus_ponens,[status(thm)],[27, 26])).
% 0.21/0.52 tff(29,plain,
% 0.21/0.52 ((~![Vdthex: $i] : ((~(ron(vd1081, Vdthex) & rcenter(vd1080, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1095))) <=> (~![Vdthex: $i] : ((~(ron(vd1081, Vdthex) & rcenter(vd1080, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1095)))),
% 0.21/0.52 inference(rewrite,[status(thm)],[])).
% 0.21/0.52 tff(30,plain,
% 0.21/0.52 ((~![Vdthex: $i] : (((ron(vd1081, Vdthex) & rcenter(vd1080, Vdthex)) & rcircle(Vdthex)) => (Vdthex = vd1095))) <=> (~![Vdthex: $i] : ((~(ron(vd1081, Vdthex) & rcenter(vd1080, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1095)))),
% 0.21/0.52 inference(rewrite,[status(thm)],[])).
% 0.21/0.52 tff(31,axiom,(~![Vdthex: $i] : (((ron(vd1081, Vdthex) & rcenter(vd1080, Vdthex)) & rcircle(Vdthex)) => (Vdthex = vd1095))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''qu(theu(the(228), 1), imp(the(228)))'')).
% 0.21/0.52 tff(32,plain,
% 0.21/0.52 (~![Vdthex: $i] : ((~(ron(vd1081, Vdthex) & rcenter(vd1080, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1095))),
% 0.21/0.52 inference(modus_ponens,[status(thm)],[31, 30])).
% 0.21/0.52 tff(33,plain,
% 0.21/0.52 (~![Vdthex: $i] : ((~(ron(vd1081, Vdthex) & rcenter(vd1080, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1095))),
% 0.21/0.52 inference(modus_ponens,[status(thm)],[32, 29])).
% 0.21/0.52 tff(34,plain,
% 0.21/0.52 (~![Vdthex: $i] : ((~(ron(vd1081, Vdthex) & rcenter(vd1080, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1095))),
% 0.21/0.52 inference(modus_ponens,[status(thm)],[33, 29])).
% 0.21/0.52 tff(35,plain,
% 0.21/0.52 (~![Vdthex: $i] : ((~(ron(vd1081, Vdthex) & rcenter(vd1080, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1095))),
% 0.21/0.52 inference(modus_ponens,[status(thm)],[34, 29])).
% 0.21/0.52 tff(36,plain,(
% 0.21/0.52 ~((~(ron(vd1081, Vdthex!0) & rcenter(vd1080, Vdthex!0) & rcircle(Vdthex!0))) | (Vdthex!0 = vd1095))),
% 0.21/0.52 inference(skolemize,[status(sab)],[35])).
% 0.21/0.52 tff(37,plain,
% 0.21/0.52 (~(Vdthex!0 = vd1095)),
% 0.21/0.52 inference(or_elim,[status(thm)],[36])).
% 0.21/0.52 tff(38,plain,
% 0.21/0.52 (ron(vd1081, Vdthex!0) & rcenter(vd1080, Vdthex!0) & rcircle(Vdthex!0)),
% 0.21/0.52 inference(or_elim,[status(thm)],[36])).
% 0.21/0.52 tff(39,plain,
% 0.21/0.52 (rcenter(vd1080, Vdthex!0)),
% 0.21/0.52 inference(and_elim,[status(thm)],[38])).
% 0.21/0.52 tff(40,plain,
% 0.21/0.52 (ron(vd1081, Vdthex!0)),
% 0.21/0.52 inference(and_elim,[status(thm)],[38])).
% 0.21/0.52 tff(41,plain,
% 0.21/0.52 (((~![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))) | ((Vdthex!0 = vd1095) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rcenter(vd1080, vd1095)))) <=> ((~![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))) | (Vdthex!0 = vd1095) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rcenter(vd1080, vd1095)))),
% 0.21/0.52 inference(rewrite,[status(thm)],[])).
% 0.21/0.52 tff(42,plain,
% 0.21/0.52 (((Vdthex!0 = vd1095) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rpoint(vd1081)) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | $false | (~rcenter(vd1080, vd1095))) <=> ((Vdthex!0 = vd1095) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rcenter(vd1080, vd1095)))),
% 0.21/0.52 inference(rewrite,[status(thm)],[])).
% 0.21/0.52 tff(43,plain,
% 0.21/0.52 ((~$true) <=> $false),
% 0.21/0.52 inference(rewrite,[status(thm)],[])).
% 0.21/0.52 tff(44,plain,
% 0.21/0.52 ((vf(vd1080, vd1081) = vf(vd1080, vd1081)) <=> $true),
% 0.21/0.52 inference(rewrite,[status(thm)],[])).
% 0.21/0.52 tff(45,plain,
% 0.21/0.52 ((~(vf(vd1080, vd1081) = vf(vd1080, vd1081))) <=> (~$true)),
% 0.21/0.52 inference(monotonicity,[status(thm)],[44])).
% 0.21/0.52 tff(46,plain,
% 0.21/0.52 ((~(vf(vd1080, vd1081) = vf(vd1080, vd1081))) <=> $false),
% 0.21/0.52 inference(transitivity,[status(thm)],[45, 43])).
% 0.21/0.52 tff(47,plain,
% 0.21/0.52 (((Vdthex!0 = vd1095) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rpoint(vd1081)) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | (~(vf(vd1080, vd1081) = vf(vd1080, vd1081))) | (~rcenter(vd1080, vd1095))) <=> ((Vdthex!0 = vd1095) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rpoint(vd1081)) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | $false | (~rcenter(vd1080, vd1095)))),
% 0.21/0.52 inference(monotonicity,[status(thm)],[46])).
% 0.21/0.52 tff(48,plain,
% 0.21/0.52 (((Vdthex!0 = vd1095) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rpoint(vd1081)) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | (~(vf(vd1080, vd1081) = vf(vd1080, vd1081))) | (~rcenter(vd1080, vd1095))) <=> ((Vdthex!0 = vd1095) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rcenter(vd1080, vd1095)))),
% 0.21/0.53 inference(transitivity,[status(thm)],[47, 42])).
% 0.21/0.53 tff(49,plain,
% 0.21/0.53 (((~![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))) | ((Vdthex!0 = vd1095) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rpoint(vd1081)) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | (~(vf(vd1080, vd1081) = vf(vd1080, vd1081))) | (~rcenter(vd1080, vd1095)))) <=> ((~![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))) | ((Vdthex!0 = vd1095) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rcenter(vd1080, vd1095))))),
% 0.21/0.53 inference(monotonicity,[status(thm)],[48])).
% 0.21/0.53 tff(50,plain,
% 0.21/0.53 (((~![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))) | ((Vdthex!0 = vd1095) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rpoint(vd1081)) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | (~(vf(vd1080, vd1081) = vf(vd1080, vd1081))) | (~rcenter(vd1080, vd1095)))) <=> ((~![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))) | (Vdthex!0 = vd1095) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rcenter(vd1080, vd1095)))),
% 0.21/0.53 inference(transitivity,[status(thm)],[49, 41])).
% 0.21/0.53 tff(51,plain,
% 0.21/0.53 ((~![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))) | ((Vdthex!0 = vd1095) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rpoint(vd1081)) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | (~(vf(vd1080, vd1081) = vf(vd1080, vd1081))) | (~rcenter(vd1080, vd1095)))),
% 0.21/0.53 inference(quant_inst,[status(thm)],[])).
% 0.21/0.53 tff(52,plain,
% 0.21/0.53 ((~![Vd837: $i, Vd838: $i, Vd842: $i, Vd843: $i, Vd844: $i] : ((Vd843 = Vd844) | (~ron(Vd837, Vd843)) | (~rpoint(Vd838)) | (~rpoint(Vd837)) | (~ron(Vd838, Vd844)) | (~rcenter(Vd842, Vd843)) | (~(vf(Vd842, Vd837) = vf(Vd842, Vd838))) | (~rcenter(Vd842, Vd844)))) | (Vdthex!0 = vd1095) | (~ron(vd1081, vd1095)) | (~rcenter(vd1080, Vdthex!0)) | (~ron(vd1081, Vdthex!0)) | (~rpoint(vd1081)) | (~rcenter(vd1080, vd1095))),
% 0.21/0.53 inference(modus_ponens,[status(thm)],[51, 50])).
% 0.21/0.53 tff(53,plain,
% 0.21/0.53 ($false),
% 0.21/0.53 inference(unit_resolution,[status(thm)],[52, 40, 39, 37, 28, 25, 20, 13])).
% 0.21/0.53 % SZS output end Proof
% 0.21/0.54 % E exiting
%------------------------------------------------------------------------------