%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : GEO272+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:40:12 AM UTC 2026
% Result : Theorem 204.64s 205.03s
% Output : Proof 204.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO272+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n009.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sat Sep 19 07:43:11 UTC 2026
% 0.07/0.34 % CPUTime :
% 204.64/205.03 % SZS status Theorem for theBenchmark
% 204.64/205.03 % SZS output start Proof for theBenchmark
% 204.64/205.03 fof(qu(theu(the(212), 1), imp(the(212))), conjecture,
% 204.64/205.03 ! [ Vdthex ] : ( ( ron(vd1055, Vdthex) & rcenter(vd1057, Vdthex) & rcircle(Vdthex) ) => Vdthex = vd1063 ),
% 204.64/205.03 file('theBenchmark.p', qu(theu(the(212), 1), imp(the(212)))) ).
% 204.64/205.03
% 204.64/205.03 fof(and(pred(comma_conjunct2(the(212)), 0), and(pred(comma_conjunct1(the(212)), 0), pred(the(212), 0))), axiom,
% 204.64/205.03 ( ron(vd1055, vd1063) & rcenter(vd1057, vd1063) & rcircle(vd1063) ),
% 204.64/205.03 file('theBenchmark.p', and(pred(comma_conjunct2(the(212)), 0), and(pred(comma_conjunct1(the(212)), 0), pred(the(212), 0)))) ).
% 204.64/205.03
% 204.64/205.03 fof(and(pred(conjunct2(210), 4), and(holds(conjunct2(210), 1059, 0), and(pred(conjunct2(210), 1), and(pred(conjunct1(210), 2), pred(conjunct1(210), 1))))), axiom,
% 204.64/205.03 ( vd1057 = vd1058 & ~( vd1055 = vd1057 ) & rpoint(vd1058) & vd1055 = vd1056 & rpoint(vd1056) ),
% 204.64/205.03 file('theBenchmark.p', and(pred(conjunct2(210), 4), and(holds(conjunct2(210), 1059, 0), and(pred(conjunct2(210), 1), and(pred(conjunct1(210), 2), pred(conjunct1(210), 1)))))) ).
% 204.64/205.03
% 204.64/205.03 fof(qu(cond(axiom(182), 0), imp(cond(axiom(182), 0))), axiom,
% 204.77/205.03 ! [ Vd837,Vd838,Vd842,Vd843,Vd844 ] : ( ( vf(Vd842, Vd837) = vf(Vd842, Vd838) & ron(Vd838, Vd844) & ron(Vd837, Vd843) & rcenter(Vd842, Vd844) & rcenter(Vd842, Vd843) & ? [ Vd841 ] : ( Vd838 = Vd841 & rpoint(Vd841) ) & ? [ Vd840 ] : ( Vd837 = Vd840 & rpoint(Vd840) ) ) => Vd843 = Vd844 ),
% 204.77/205.03 file('theBenchmark.p', qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))) ).
% 204.77/205.03
% 204.77/205.03 fof(f_1_1, negated_conjecture,
% 204.77/205.03 ~( ! [ Vdthex ] : ( ( ron(vd1055, Vdthex) & rcenter(vd1057, Vdthex) & rcircle(Vdthex) ) => Vdthex = vd1063 ) ),
% 204.77/205.03 inference(negate,[status(cth)],[qu(theu(the(212), 1), imp(the(212)))]) ).
% 204.77/205.03
% 204.77/205.03 fof(f_1_2, negated_conjecture,
% 204.77/205.03 ? [ Vdthex ] : ( ( ron(vd1055, Vdthex) & rcenter(vd1057, Vdthex) & rcircle(Vdthex) ) & ~( Vdthex = vd1063 ) ),
% 204.77/205.03 inference(fof_nnf,[status(thm)],[f_1_1]) ).
% 204.77/205.03
% 204.77/205.03 fof(f_1_3, negated_conjecture,
% 204.77/205.03 ? [ U_0 ] : ( ( ron(vd1055, U_0) & rcenter(vd1057, U_0) & rcircle(U_0) ) & ~( U_0 = vd1063 ) ),
% 204.77/205.03 inference(variable_rename,[status(thm)],[f_1_2]) ).
% 204.77/205.03
% 204.77/205.03 fof(f_1_4, negated_conjecture,
% 204.77/205.03 ( ( ron(vd1055, sK1) & rcenter(vd1057, sK1) & rcircle(sK1) ) & ~( sK1 = vd1063 ) ),
% 204.77/205.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_0,sK1)],[f_1_3]) ).
% 204.77/205.03
% 204.77/205.03 fof(f_1_5, negated_conjecture,
% 204.77/205.03 ( ( ( ron(vd1055, sK1) ) ) & ( ( rcenter(vd1057, sK1) ) ) & ( ( rcircle(sK1) ) ) & ( ( sK1 != vd1063 ) ) ),
% 204.77/205.03 inference(definitional_conversion,[status(esa)],[f_1_4]) ).
% 204.77/205.03
% 204.77/205.03 cnf(f_1_6, negated_conjecture,
% 204.77/205.03 ( ron(vd1055, sK1) ),
% 204.77/205.03 inference(clausify,[status(thm)],[f_1_5]) ).
% 204.77/205.03
% 204.77/205.03 cnf(f_1_7, negated_conjecture,
% 204.77/205.03 ( rcenter(vd1057, sK1) ),
% 204.77/205.03 inference(clausify,[status(thm)],[f_1_5]) ).
% 204.77/205.03
% 204.77/205.03 cnf(f_1_9, negated_conjecture,
% 204.77/205.03 ( sK1 != vd1063 ),
% 204.77/205.03 inference(clausify,[status(thm)],[f_1_5]) ).
% 204.77/205.03
% 204.77/205.03 fof(f_2_1, plain,
% 204.77/205.03 ( ron(vd1055, vd1063) & rcenter(vd1057, vd1063) & rcircle(vd1063) ),
% 204.77/205.03 inference(fof_nnf,[status(thm)],[and(pred(comma_conjunct2(the(212)), 0), and(pred(comma_conjunct1(the(212)), 0), pred(the(212), 0)))]) ).
% 204.77/205.03
% 204.77/205.03 fof(f_2_2, plain,
% 204.77/205.03 ( ( ( ron(vd1055, vd1063) ) ) & ( ( rcenter(vd1057, vd1063) ) ) & ( ( rcircle(vd1063) ) ) ),
% 204.77/205.03 inference(definitional_conversion,[status(esa)],[f_2_1]) ).
% 204.77/205.03
% 204.77/205.03 cnf(f_2_3, plain,
% 204.77/205.03 ( ron(vd1055, vd1063) ),
% 204.77/205.03 inference(clausify,[status(thm)],[f_2_2]) ).
% 204.77/205.03
% 204.77/205.03 cnf(f_2_4, plain,
% 204.77/205.03 ( rcenter(vd1057, vd1063) ),
% 204.77/205.03 inference(clausify,[status(thm)],[f_2_2]) ).
% 204.77/205.03
% 204.77/205.03 fof(f_6_1, plain,
% 204.77/205.03 ( vd1057 = vd1058 & ~( vd1055 = vd1057 ) & rpoint(vd1058) & vd1055 = vd1056 & rpoint(vd1056) ),
% 204.77/205.03 inference(fof_nnf,[status(thm)],[and(pred(conjunct2(210), 4), and(holds(conjunct2(210), 1059, 0), and(pred(conjunct2(210), 1), and(pred(conjunct1(210), 2), pred(conjunct1(210), 1)))))]) ).
% 204.77/205.03
% 204.77/205.03 fof(f_6_2, plain,
% 204.77/205.03 ( ( ( vd1057 = vd1058 ) ) & ( ( vd1055 != vd1057 ) ) & ( ( rpoint(vd1058) ) ) & ( ( vd1055 = vd1056 ) ) & ( ( rpoint(vd1056) ) ) ),
% 204.77/205.03 inference(definitional_conversion,[status(esa)],[f_6_1]) ).
% 204.77/205.03
% 204.77/205.03 cnf(f_6_6, plain,
% 204.77/205.03 ( vd1055 = vd1056 ),
% 204.77/205.03 inference(clausify,[status(thm)],[f_6_2]) ).
% 204.77/205.03
% 204.77/205.03 cnf(f_6_7, plain,
% 204.77/205.03 ( rpoint(vd1056) ),
% 204.77/205.03 inference(clausify,[status(thm)],[f_6_2]) ).
% 204.77/205.03
% 204.77/205.03 fof(f_9_1, plain,
% 204.77/205.03 ! [ Vd837,Vd838,Vd842,Vd843,Vd844 ] : ( ( ~( vf(Vd842, Vd837) = vf(Vd842, Vd838) ) | ~( ron(Vd838, Vd844) ) | ~( ron(Vd837, Vd843) ) | ~( rcenter(Vd842, Vd844) ) | ~( rcenter(Vd842, Vd843) ) | ! [ Vd841 ] : ( ~( Vd838 = Vd841 ) | ~( rpoint(Vd841) ) ) | ! [ Vd840 ] : ( ~( Vd837 = Vd840 ) | ~( rpoint(Vd840) ) ) ) | Vd843 = Vd844 ),
% 204.77/205.03 inference(fof_nnf,[status(thm)],[qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))]) ).
% 204.77/205.03
% 204.77/205.03 fof(f_9_2, plain,
% 204.77/205.03 ! [ U_19,U_18,U_17,U_16,U_15 ] : ( ( ~( vf(U_17, U_19) = vf(U_17, U_18) ) | ~( ron(U_18, U_15) ) | ~( ron(U_19, U_16) ) | ~( rcenter(U_17, U_15) ) | ~( rcenter(U_17, U_16) ) | ! [ U_13 ] : ( ~( U_18 = U_13 ) | ~( rpoint(U_13) ) ) | ! [ U_14 ] : ( ~( U_19 = U_14 ) | ~( rpoint(U_14) ) ) ) | U_16 = U_15 ),
% 204.77/205.03 inference(variable_rename,[status(thm)],[f_9_1]) ).
% 204.77/205.03
% 204.77/205.03 fof(f_9_3, plain,
% 204.77/205.03 ( ( ! [U_15, U_16, U_14, U_18, U_13, U_19, U_17] : ( vf(U_17, U_19) != vf(U_17, U_18) | ~ron(U_18, U_15) | ~ron(U_19, U_16) | ~rcenter(U_17, U_15) | ~rcenter(U_17, U_16) | U_18 != U_13 | ~rpoint(U_13) | U_19 != U_14 | ~rpoint(U_14) | U_16 = U_15 ) ) ),
% 204.77/205.03 inference(definitional_conversion,[status(esa)],[f_9_2]) ).
% 204.77/205.03
% 204.77/205.03 cnf(f_9_4, plain,
% 204.77/205.03 ( vf(U_17, U_19) != vf(U_17, U_18) | ~ron(U_18, U_15) | ~ron(U_19, U_16) | ~rcenter(U_17, U_15) | ~rcenter(U_17, U_16) | U_18 != U_13 | ~rpoint(U_13) | U_19 != U_14 | ~rpoint(U_14) | U_16 = U_15 ),
% 204.77/205.03 inference(clausify,[status(thm)],[f_9_3]) ).
% 204.77/205.03
% 204.77/205.03 cnf(equality_1, axiom,
% 204.77/205.03 ( Eq_x_0 = Eq_x_0 ),
% 204.77/205.03 theory(equality,[reflexivity]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t1, plain, ( sK1 != vd1063 ),
% 204.77/205.03 inference(start, [status(thm), parent(0:0)], [f_1_9]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t2, plain, ( sK1 = vd1063 | ~ron(vd1055, sK1) | vd1055 != vd1056 | vd1055 != vd1056 | ~rpoint(vd1056) | ~ron(vd1055, vd1063) | ~rpoint(vd1056) | ~rcenter(vd1057, sK1) | ~rcenter(vd1057, vd1063) | vf(vd1057, vd1055) != vf(vd1057, vd1055) ),
% 204.77/205.03 inference(extension, [status(thm), parent(t1:1)], [f_9_4]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t3, plain, $false,
% 204.77/205.03 inference(connection, [status(thm), parent(t2:1)], [t2:1,t1:1]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t4, plain, ( ron(vd1055, sK1) ),
% 204.77/205.03 inference(extension, [status(thm), parent(t2:2)], [f_1_6]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t5, plain, $false,
% 204.77/205.03 inference(connection, [status(thm), parent(t4:1)], [t4:1,t2:2]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t6, plain, ( vd1055 = vd1056 ),
% 204.77/205.03 inference(extension, [status(thm), parent(t2:3)], [f_6_6]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t7, plain, $false,
% 204.77/205.03 inference(connection, [status(thm), parent(t6:1)], [t6:1,t2:3]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t8, plain, ( vd1055 = vd1056 ),
% 204.77/205.03 inference(extension, [status(thm), parent(t2:4)], [f_6_6]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t9, plain, $false,
% 204.77/205.03 inference(connection, [status(thm), parent(t8:1)], [t8:1,t2:4]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t10, plain, ( rpoint(vd1056) ),
% 204.77/205.03 inference(extension, [status(thm), parent(t2:5)], [f_6_7]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t11, plain, $false,
% 204.77/205.03 inference(connection, [status(thm), parent(t10:1)], [t10:1,t2:5]) ).
% 204.77/205.03
% 204.77/205.03 cnf(l5, lemma, rpoint(vd1056),
% 204.77/205.03 inference(lemma, [status(cth), parent(t2:5), below(t1:1)], [t2:5]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t12, plain, ( ron(vd1055, vd1063) ),
% 204.77/205.03 inference(extension, [status(thm), parent(t2:6)], [f_2_3]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t13, plain, $false,
% 204.77/205.03 inference(connection, [status(thm), parent(t12:1)], [t12:1,t2:6]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t14, plain, rpoint(vd1056),
% 204.77/205.03 inference(lemma_extension, [status(thm), parent(t2:7)], [l5:1]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t15, plain, $false,
% 204.77/205.03 inference(connection, [status(thm), parent(t14:1)], [t14:1,t2:7]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t16, plain, ( rcenter(vd1057, sK1) ),
% 204.77/205.03 inference(extension, [status(thm), parent(t2:8)], [f_1_7]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t17, plain, $false,
% 204.77/205.03 inference(connection, [status(thm), parent(t16:1)], [t16:1,t2:8]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t18, plain, ( rcenter(vd1057, vd1063) ),
% 204.77/205.03 inference(extension, [status(thm), parent(t2:9)], [f_2_4]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t19, plain, $false,
% 204.77/205.03 inference(connection, [status(thm), parent(t18:1)], [t18:1,t2:9]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t20, plain, ( vf(vd1057, vd1055) = vf(vd1057, vd1055) ),
% 204.77/205.03 inference(extension, [status(thm), parent(t2:10)], [equality_1]) ).
% 204.77/205.03
% 204.77/205.03 cnf(t21, plain, $false,
% 204.77/205.03 inference(connection, [status(thm), parent(t20:1)], [t20:1,t2:10]) ).
% 204.77/205.03
% 204.77/205.03 % SZS output end Proof for theBenchmark
%------------------------------------------------------------------------------