%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : GEO278+1 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n015.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.41s 0.57s
% Output : Proof 0.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO278+1 : TPTP v9.0.0. Released v4.1.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n015.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu Jun 19 14:44:10 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.41/0.57 % SZS status Theorem
% 0.41/0.57 % SZS output start Proof
% 0.41/0.57 tff(rcenter_type, type, (
% 0.41/0.57 rcenter: ( $i * $i ) > $o)).
% 0.41/0.57 tff(vf_type, type, (
% 0.41/0.57 vf: ( $i * $i ) > $i)).
% 0.41/0.57 tff(ron_type, type, (
% 0.41/0.57 ron: ( $i * $i ) > $o)).
% 0.41/0.57 tff(rpoint_type, type, (
% 0.41/0.57 rpoint: $i > $o)).
% 0.41/0.57 tff(vd1096_type, type, (
% 0.41/0.57 vd1096: $i)).
% 0.41/0.57 tff(vd1102_type, type, (
% 0.41/0.57 vd1102: $i)).
% 0.41/0.57 tff(vd1089_type, type, (
% 0.41/0.57 vd1089: $i)).
% 0.41/0.57 tff(rcircle_type, type, (
% 0.41/0.57 rcircle: $i > $o)).
% 0.41/0.57 tff(tptp_fun_Vdthex_0_type, type, (
% 0.41/0.57 tptp_fun_Vdthex_0: $i)).
% 0.41/0.57 tff(1,plain,
% 0.41/0.57 (^[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.41/0.57 inference(bind,[status(th)],[])).
% 0.41/0.57 tff(2,plain,
% 0.41/0.57 (![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.41/0.57 inference(quant_intro,[status(thm)],[1])).
% 0.41/0.57 tff(3,plain,
% 0.41/0.57 (^[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.41/0.57 inference(bind,[status(th)],[])).
% 0.41/0.57 tff(4,plain,
% 0.41/0.57 (![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.41/0.57 inference(quant_intro,[status(thm)],[3])).
% 0.41/0.57 tff(5,plain,
% 0.41/0.57 (![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.41/0.57 inference(rewrite,[status(thm)],[])).
% 0.41/0.57 tff(6,plain,
% 0.41/0.57 (^[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.41/0.57 inference(bind,[status(th)],[])).
% 0.41/0.57 tff(7,plain,
% 0.41/0.57 (![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.41/0.57 inference(quant_intro,[status(thm)],[6])).
% 0.41/0.57 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.41/0.57 tff(9,plain,
% 0.41/0.57 (![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.41/0.57 inference(modus_ponens,[status(thm)],[8, 7])).
% 0.41/0.57 tff(10,plain,
% 0.41/0.57 (![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.41/0.57 inference(modus_ponens,[status(thm)],[9, 5])).
% 0.41/0.57 tff(11,plain,(
% 0.41/0.57 ![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.41/0.57 inference(skolemize,[status(sab)],[10])).
% 0.41/0.57 tff(12,plain,
% 0.41/0.57 (![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.41/0.57 inference(modus_ponens,[status(thm)],[11, 4])).
% 0.41/0.57 tff(13,plain,
% 0.41/0.57 (![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.41/0.57 inference(modus_ponens,[status(thm)],[12, 2])).
% 0.41/0.57 tff(14,plain,
% 0.41/0.57 (rpoint(vd1096) <=> rpoint(vd1096)),
% 0.41/0.57 inference(rewrite,[status(thm)],[])).
% 0.41/0.57 tff(15,axiom,(rpoint(vd1096)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''pred(229, 0)'')).
% 0.41/0.57 tff(16,plain,
% 0.41/0.57 (rpoint(vd1096)),
% 0.41/0.57 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.41/0.57 tff(17,plain,
% 0.41/0.57 (rcenter(vd1089, vd1102) <=> rcenter(vd1089, vd1102)),
% 0.41/0.57 inference(rewrite,[status(thm)],[])).
% 0.41/0.57 tff(18,axiom,((ron(vd1096, vd1102) & rcenter(vd1089, vd1102)) & rcircle(vd1102)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''and(pred(comma_conjunct2(the(231)), 0), and(pred(comma_conjunct1(the(231)), 0), pred(the(231), 0)))'')).
% 0.41/0.57 tff(19,plain,
% 0.41/0.57 (ron(vd1096, vd1102) & rcenter(vd1089, vd1102)),
% 0.41/0.57 inference(and_elim,[status(thm)],[18])).
% 0.41/0.57 tff(20,plain,
% 0.41/0.57 (rcenter(vd1089, vd1102)),
% 0.41/0.57 inference(and_elim,[status(thm)],[19])).
% 0.41/0.57 tff(21,plain,
% 0.41/0.57 (rcenter(vd1089, vd1102)),
% 0.41/0.57 inference(modus_ponens,[status(thm)],[20, 17])).
% 0.41/0.57 tff(22,plain,
% 0.41/0.57 (ron(vd1096, vd1102) <=> ron(vd1096, vd1102)),
% 0.41/0.57 inference(rewrite,[status(thm)],[])).
% 0.41/0.57 tff(23,plain,
% 0.41/0.57 (ron(vd1096, vd1102)),
% 0.41/0.57 inference(and_elim,[status(thm)],[19])).
% 0.41/0.57 tff(24,plain,
% 0.41/0.57 (ron(vd1096, vd1102)),
% 0.41/0.57 inference(modus_ponens,[status(thm)],[23, 22])).
% 0.41/0.57 tff(25,plain,
% 0.41/0.57 ((~![Vdthex: $i] : ((~(ron(vd1096, Vdthex) & rcenter(vd1089, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1102))) <=> (~![Vdthex: $i] : ((~(ron(vd1096, Vdthex) & rcenter(vd1089, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1102)))),
% 0.41/0.57 inference(rewrite,[status(thm)],[])).
% 0.41/0.57 tff(26,plain,
% 0.41/0.57 ((~![Vdthex: $i] : (((ron(vd1096, Vdthex) & rcenter(vd1089, Vdthex)) & rcircle(Vdthex)) => (Vdthex = vd1102))) <=> (~![Vdthex: $i] : ((~(ron(vd1096, Vdthex) & rcenter(vd1089, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1102)))),
% 0.41/0.57 inference(rewrite,[status(thm)],[])).
% 0.41/0.57 tff(27,axiom,(~![Vdthex: $i] : (((ron(vd1096, Vdthex) & rcenter(vd1089, Vdthex)) & rcircle(Vdthex)) => (Vdthex = vd1102))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''qu(theu(the(231), 1), imp(the(231)))'')).
% 0.41/0.57 tff(28,plain,
% 0.41/0.57 (~![Vdthex: $i] : ((~(ron(vd1096, Vdthex) & rcenter(vd1089, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1102))),
% 0.41/0.57 inference(modus_ponens,[status(thm)],[27, 26])).
% 0.41/0.57 tff(29,plain,
% 0.41/0.57 (~![Vdthex: $i] : ((~(ron(vd1096, Vdthex) & rcenter(vd1089, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1102))),
% 0.41/0.57 inference(modus_ponens,[status(thm)],[28, 25])).
% 0.41/0.57 tff(30,plain,
% 0.41/0.57 (~![Vdthex: $i] : ((~(ron(vd1096, Vdthex) & rcenter(vd1089, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1102))),
% 0.41/0.58 inference(modus_ponens,[status(thm)],[29, 25])).
% 0.41/0.58 tff(31,plain,
% 0.41/0.58 (~![Vdthex: $i] : ((~(ron(vd1096, Vdthex) & rcenter(vd1089, Vdthex) & rcircle(Vdthex))) | (Vdthex = vd1102))),
% 0.41/0.58 inference(modus_ponens,[status(thm)],[30, 25])).
% 0.41/0.58 tff(32,plain,(
% 0.41/0.58 ~((~(ron(vd1096, Vdthex!0) & rcenter(vd1089, Vdthex!0) & rcircle(Vdthex!0))) | (Vdthex!0 = vd1102))),
% 0.41/0.58 inference(skolemize,[status(sab)],[31])).
% 0.41/0.58 tff(33,plain,
% 0.41/0.58 (~(Vdthex!0 = vd1102)),
% 0.41/0.58 inference(or_elim,[status(thm)],[32])).
% 0.41/0.58 tff(34,plain,
% 0.41/0.58 (ron(vd1096, Vdthex!0) & rcenter(vd1089, Vdthex!0) & rcircle(Vdthex!0)),
% 0.41/0.58 inference(or_elim,[status(thm)],[32])).
% 0.41/0.58 tff(35,plain,
% 0.41/0.58 (rcenter(vd1089, Vdthex!0)),
% 0.41/0.58 inference(and_elim,[status(thm)],[34])).
% 0.41/0.58 tff(36,plain,
% 0.41/0.58 (ron(vd1096, Vdthex!0)),
% 0.41/0.58 inference(and_elim,[status(thm)],[34])).
% 0.41/0.58 tff(37,plain,
% 0.41/0.58 (((~![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 = vd1102) | (~rpoint(vd1096)) | (~ron(vd1096, Vdthex!0)) | (~rcenter(vd1089, Vdthex!0)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, vd1102)))) <=> ((~![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 = vd1102) | (~rpoint(vd1096)) | (~ron(vd1096, Vdthex!0)) | (~rcenter(vd1089, Vdthex!0)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, vd1102)))),
% 0.41/0.58 inference(rewrite,[status(thm)],[])).
% 0.41/0.58 tff(38,plain,
% 0.41/0.58 (((Vdthex!0 = vd1102) | (~ron(vd1096, Vdthex!0)) | (~rpoint(vd1096)) | (~rpoint(vd1096)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, Vdthex!0)) | $false | (~rcenter(vd1089, vd1102))) <=> ((Vdthex!0 = vd1102) | (~rpoint(vd1096)) | (~ron(vd1096, Vdthex!0)) | (~rcenter(vd1089, Vdthex!0)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, vd1102)))),
% 0.41/0.58 inference(rewrite,[status(thm)],[])).
% 0.41/0.58 tff(39,plain,
% 0.41/0.58 ((~$true) <=> $false),
% 0.41/0.58 inference(rewrite,[status(thm)],[])).
% 0.41/0.58 tff(40,plain,
% 0.41/0.58 ((vf(vd1089, vd1096) = vf(vd1089, vd1096)) <=> $true),
% 0.41/0.58 inference(rewrite,[status(thm)],[])).
% 0.41/0.58 tff(41,plain,
% 0.41/0.58 ((~(vf(vd1089, vd1096) = vf(vd1089, vd1096))) <=> (~$true)),
% 0.41/0.58 inference(monotonicity,[status(thm)],[40])).
% 0.41/0.58 tff(42,plain,
% 0.41/0.58 ((~(vf(vd1089, vd1096) = vf(vd1089, vd1096))) <=> $false),
% 0.41/0.58 inference(transitivity,[status(thm)],[41, 39])).
% 0.41/0.58 tff(43,plain,
% 0.41/0.58 (((Vdthex!0 = vd1102) | (~ron(vd1096, Vdthex!0)) | (~rpoint(vd1096)) | (~rpoint(vd1096)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, Vdthex!0)) | (~(vf(vd1089, vd1096) = vf(vd1089, vd1096))) | (~rcenter(vd1089, vd1102))) <=> ((Vdthex!0 = vd1102) | (~ron(vd1096, Vdthex!0)) | (~rpoint(vd1096)) | (~rpoint(vd1096)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, Vdthex!0)) | $false | (~rcenter(vd1089, vd1102)))),
% 0.41/0.58 inference(monotonicity,[status(thm)],[42])).
% 0.41/0.58 tff(44,plain,
% 0.41/0.58 (((Vdthex!0 = vd1102) | (~ron(vd1096, Vdthex!0)) | (~rpoint(vd1096)) | (~rpoint(vd1096)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, Vdthex!0)) | (~(vf(vd1089, vd1096) = vf(vd1089, vd1096))) | (~rcenter(vd1089, vd1102))) <=> ((Vdthex!0 = vd1102) | (~rpoint(vd1096)) | (~ron(vd1096, Vdthex!0)) | (~rcenter(vd1089, Vdthex!0)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, vd1102)))),
% 0.41/0.58 inference(transitivity,[status(thm)],[43, 38])).
% 0.41/0.58 tff(45,plain,
% 0.41/0.58 (((~![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 = vd1102) | (~ron(vd1096, Vdthex!0)) | (~rpoint(vd1096)) | (~rpoint(vd1096)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, Vdthex!0)) | (~(vf(vd1089, vd1096) = vf(vd1089, vd1096))) | (~rcenter(vd1089, vd1102)))) <=> ((~![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 = vd1102) | (~rpoint(vd1096)) | (~ron(vd1096, Vdthex!0)) | (~rcenter(vd1089, Vdthex!0)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, vd1102))))),
% 0.44/0.59 inference(monotonicity,[status(thm)],[44])).
% 0.44/0.59 tff(46,plain,
% 0.44/0.59 (((~![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 = vd1102) | (~ron(vd1096, Vdthex!0)) | (~rpoint(vd1096)) | (~rpoint(vd1096)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, Vdthex!0)) | (~(vf(vd1089, vd1096) = vf(vd1089, vd1096))) | (~rcenter(vd1089, vd1102)))) <=> ((~![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 = vd1102) | (~rpoint(vd1096)) | (~ron(vd1096, Vdthex!0)) | (~rcenter(vd1089, Vdthex!0)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, vd1102)))),
% 0.44/0.59 inference(transitivity,[status(thm)],[45, 37])).
% 0.44/0.59 tff(47,plain,
% 0.44/0.59 ((~![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 = vd1102) | (~ron(vd1096, Vdthex!0)) | (~rpoint(vd1096)) | (~rpoint(vd1096)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, Vdthex!0)) | (~(vf(vd1089, vd1096) = vf(vd1089, vd1096))) | (~rcenter(vd1089, vd1102)))),
% 0.44/0.59 inference(quant_inst,[status(thm)],[])).
% 0.44/0.59 tff(48,plain,
% 0.44/0.59 ((~![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 = vd1102) | (~rpoint(vd1096)) | (~ron(vd1096, Vdthex!0)) | (~rcenter(vd1089, Vdthex!0)) | (~ron(vd1096, vd1102)) | (~rcenter(vd1089, vd1102))),
% 0.44/0.59 inference(modus_ponens,[status(thm)],[47, 46])).
% 0.44/0.59 tff(49,plain,
% 0.44/0.59 ($false),
% 0.44/0.59 inference(unit_resolution,[status(thm)],[48, 36, 35, 33, 24, 21, 16, 13])).
% 0.44/0.59 % SZS output end Proof
% 0.44/0.59 % E exiting
%------------------------------------------------------------------------------