%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : GEO275+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 222.36s 222.68s
% Output : Proof 222.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO275+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n020.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:47 UTC 2026
% 0.07/0.35 % CPUTime :
% 222.36/222.68 % SZS status Theorem for theBenchmark
% 222.36/222.68 % SZS output start Proof for theBenchmark
% 222.36/222.68 fof(qu(theu(the(228), 1), imp(the(228))), conjecture,
% 222.36/222.68 ! [ Vdthex ] : ( ( ron(vd1081, Vdthex) & rcenter(vd1080, Vdthex) & rcircle(Vdthex) ) => Vdthex = vd1095 ),
% 222.36/222.68 file('theBenchmark.p', qu(theu(the(228), 1), imp(the(228)))) ).
% 222.36/222.68
% 222.36/222.68 fof(and(pred(comma_conjunct2(the(228)), 0), and(pred(comma_conjunct1(the(228)), 0), pred(the(228), 0))), axiom,
% 222.36/222.68 ( ron(vd1081, vd1095) & rcenter(vd1080, vd1095) & rcircle(vd1095) ),
% 222.36/222.68 file('theBenchmark.p', and(pred(comma_conjunct2(the(228)), 0), and(pred(comma_conjunct1(the(228)), 0), pred(the(228), 0)))) ).
% 222.36/222.68
% 222.36/222.68 fof(qe(s2(plural(224))), axiom,
% 222.36/222.68 ? [ Vd1084 ] : ( vd1081 = Vd1084 & rpoint(Vd1084) ),
% 222.36/222.68 file('theBenchmark.p', qe(s2(plural(224)))) ).
% 222.36/222.68
% 222.36/222.68 fof(qu(cond(axiom(182), 0), imp(cond(axiom(182), 0))), axiom,
% 222.36/222.68 ! [ 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 ),
% 222.36/222.68 file('theBenchmark.p', qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))) ).
% 222.36/222.68
% 222.36/222.68 fof(f_1_1, negated_conjecture,
% 222.36/222.68 ~( ! [ Vdthex ] : ( ( ron(vd1081, Vdthex) & rcenter(vd1080, Vdthex) & rcircle(Vdthex) ) => Vdthex = vd1095 ) ),
% 222.36/222.68 inference(negate,[status(cth)],[qu(theu(the(228), 1), imp(the(228)))]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_1_2, negated_conjecture,
% 222.36/222.68 ? [ Vdthex ] : ( ( ron(vd1081, Vdthex) & rcenter(vd1080, Vdthex) & rcircle(Vdthex) ) & ~( Vdthex = vd1095 ) ),
% 222.36/222.68 inference(fof_nnf,[status(thm)],[f_1_1]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_1_3, negated_conjecture,
% 222.36/222.68 ? [ U_0 ] : ( ( ron(vd1081, U_0) & rcenter(vd1080, U_0) & rcircle(U_0) ) & ~( U_0 = vd1095 ) ),
% 222.36/222.68 inference(variable_rename,[status(thm)],[f_1_2]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_1_4, negated_conjecture,
% 222.36/222.68 ( ( ron(vd1081, sK1) & rcenter(vd1080, sK1) & rcircle(sK1) ) & ~( sK1 = vd1095 ) ),
% 222.36/222.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_0,sK1)],[f_1_3]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_1_5, negated_conjecture,
% 222.36/222.68 ( ( ( ron(vd1081, sK1) ) ) & ( ( rcenter(vd1080, sK1) ) ) & ( ( rcircle(sK1) ) ) & ( ( sK1 != vd1095 ) ) ),
% 222.36/222.68 inference(definitional_conversion,[status(esa)],[f_1_4]) ).
% 222.36/222.68
% 222.36/222.68 cnf(f_1_6, negated_conjecture,
% 222.36/222.68 ( ron(vd1081, sK1) ),
% 222.36/222.68 inference(clausify,[status(thm)],[f_1_5]) ).
% 222.36/222.68
% 222.36/222.68 cnf(f_1_7, negated_conjecture,
% 222.36/222.68 ( rcenter(vd1080, sK1) ),
% 222.36/222.68 inference(clausify,[status(thm)],[f_1_5]) ).
% 222.36/222.68
% 222.36/222.68 cnf(f_1_9, negated_conjecture,
% 222.36/222.68 ( sK1 != vd1095 ),
% 222.36/222.68 inference(clausify,[status(thm)],[f_1_5]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_2_1, plain,
% 222.36/222.68 ( ron(vd1081, vd1095) & rcenter(vd1080, vd1095) & rcircle(vd1095) ),
% 222.36/222.68 inference(fof_nnf,[status(thm)],[and(pred(comma_conjunct2(the(228)), 0), and(pred(comma_conjunct1(the(228)), 0), pred(the(228), 0)))]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_2_2, plain,
% 222.36/222.68 ( ( ( ron(vd1081, vd1095) ) ) & ( ( rcenter(vd1080, vd1095) ) ) & ( ( rcircle(vd1095) ) ) ),
% 222.36/222.68 inference(definitional_conversion,[status(esa)],[f_2_1]) ).
% 222.36/222.68
% 222.36/222.68 cnf(f_2_3, plain,
% 222.36/222.68 ( ron(vd1081, vd1095) ),
% 222.36/222.68 inference(clausify,[status(thm)],[f_2_2]) ).
% 222.36/222.68
% 222.36/222.68 cnf(f_2_4, plain,
% 222.36/222.68 ( rcenter(vd1080, vd1095) ),
% 222.36/222.68 inference(clausify,[status(thm)],[f_2_2]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_7_1, plain,
% 222.36/222.68 ? [ Vd1084 ] : ( vd1081 = Vd1084 & rpoint(Vd1084) ),
% 222.36/222.68 inference(fof_nnf,[status(thm)],[qe(s2(plural(224)))]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_7_2, plain,
% 222.36/222.68 ? [ U_2 ] : ( vd1081 = U_2 & rpoint(U_2) ),
% 222.36/222.68 inference(variable_rename,[status(thm)],[f_7_1]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_7_3, plain,
% 222.36/222.68 ( vd1081 = sK2 & rpoint(sK2) ),
% 222.36/222.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_2,sK2)],[f_7_2]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_7_4, plain,
% 222.36/222.68 ( ( ( vd1081 = sK2 ) ) & ( ( rpoint(sK2) ) ) ),
% 222.36/222.68 inference(definitional_conversion,[status(esa)],[f_7_3]) ).
% 222.36/222.68
% 222.36/222.68 cnf(f_7_5, plain,
% 222.36/222.68 ( vd1081 = sK2 ),
% 222.36/222.68 inference(clausify,[status(thm)],[f_7_4]) ).
% 222.36/222.68
% 222.36/222.68 cnf(f_7_6, plain,
% 222.36/222.68 ( rpoint(sK2) ),
% 222.36/222.68 inference(clausify,[status(thm)],[f_7_4]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_106_1, plain,
% 222.36/222.68 ! [ 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 ),
% 222.36/222.68 inference(fof_nnf,[status(thm)],[qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_106_2, plain,
% 222.36/222.68 ! [ U_622,U_621,U_620,U_619,U_618 ] : ( ( ~( vf(U_620, U_622) = vf(U_620, U_621) ) | ~( ron(U_621, U_618) ) | ~( ron(U_622, U_619) ) | ~( rcenter(U_620, U_618) ) | ~( rcenter(U_620, U_619) ) | ! [ U_616 ] : ( ~( U_621 = U_616 ) | ~( rpoint(U_616) ) ) | ! [ U_617 ] : ( ~( U_622 = U_617 ) | ~( rpoint(U_617) ) ) ) | U_619 = U_618 ),
% 222.36/222.68 inference(variable_rename,[status(thm)],[f_106_1]) ).
% 222.36/222.68
% 222.36/222.68 fof(f_106_3, plain,
% 222.36/222.68 ( ( ! [U_620, U_617, U_618, U_621, U_619, U_616, U_622] : ( vf(U_620, U_622) != vf(U_620, U_621) | ~ron(U_621, U_618) | ~ron(U_622, U_619) | ~rcenter(U_620, U_618) | ~rcenter(U_620, U_619) | U_621 != U_616 | ~rpoint(U_616) | U_622 != U_617 | ~rpoint(U_617) | U_619 = U_618 ) ) ),
% 222.36/222.68 inference(definitional_conversion,[status(esa)],[f_106_2]) ).
% 222.36/222.68
% 222.36/222.68 cnf(f_106_4, plain,
% 222.36/222.68 ( vf(U_620, U_622) != vf(U_620, U_621) | ~ron(U_621, U_618) | ~ron(U_622, U_619) | ~rcenter(U_620, U_618) | ~rcenter(U_620, U_619) | U_621 != U_616 | ~rpoint(U_616) | U_622 != U_617 | ~rpoint(U_617) | U_619 = U_618 ),
% 222.36/222.68 inference(clausify,[status(thm)],[f_106_3]) ).
% 222.36/222.68
% 222.36/222.68 cnf(equality_1, axiom,
% 222.36/222.68 ( Eq_x_0 = Eq_x_0 ),
% 222.36/222.68 theory(equality,[reflexivity]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t1, plain, ( sK1 != vd1095 ),
% 222.36/222.68 inference(start, [status(thm), parent(0:0)], [f_1_9]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t2, plain, ( sK1 = vd1095 | ~rpoint(sK2) | ~rpoint(sK2) | ~rcenter(vd1080, sK1) | ~ron(vd1081, vd1095) | vf(vd1080, vd1081) != vf(vd1080, vd1081) | vd1081 != sK2 | ~rcenter(vd1080, vd1095) | vd1081 != sK2 | ~ron(vd1081, sK1) ),
% 222.36/222.68 inference(extension, [status(thm), parent(t1:1)], [f_106_4]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t3, plain, $false,
% 222.36/222.68 inference(connection, [status(thm), parent(t2:1)], [t2:1,t1:1]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t4, plain, ( rpoint(sK2) ),
% 222.36/222.68 inference(extension, [status(thm), parent(t2:2)], [f_7_6]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t5, plain, $false,
% 222.36/222.68 inference(connection, [status(thm), parent(t4:1)], [t4:1,t2:2]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t6, plain, ( rpoint(sK2) ),
% 222.36/222.68 inference(extension, [status(thm), parent(t2:3)], [f_7_6]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t7, plain, $false,
% 222.36/222.68 inference(connection, [status(thm), parent(t6:1)], [t6:1,t2:3]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t8, plain, ( rcenter(vd1080, sK1) ),
% 222.36/222.68 inference(extension, [status(thm), parent(t2:4)], [f_1_7]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t9, plain, $false,
% 222.36/222.68 inference(connection, [status(thm), parent(t8:1)], [t8:1,t2:4]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t10, plain, ( ron(vd1081, vd1095) ),
% 222.36/222.68 inference(extension, [status(thm), parent(t2:5)], [f_2_3]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t11, plain, $false,
% 222.36/222.68 inference(connection, [status(thm), parent(t10:1)], [t10:1,t2:5]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t12, plain, ( vf(vd1080, vd1081) = vf(vd1080, vd1081) ),
% 222.36/222.68 inference(extension, [status(thm), parent(t2:6)], [equality_1]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t13, plain, $false,
% 222.36/222.68 inference(connection, [status(thm), parent(t12:1)], [t12:1,t2:6]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t14, plain, ( vd1081 = sK2 ),
% 222.36/222.68 inference(extension, [status(thm), parent(t2:7)], [f_7_5]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t15, plain, $false,
% 222.36/222.68 inference(connection, [status(thm), parent(t14:1)], [t14:1,t2:7]) ).
% 222.36/222.68
% 222.36/222.68 cnf(l7, lemma, vd1081 = sK2,
% 222.36/222.68 inference(lemma, [status(cth), parent(t2:7), below(t1:1)], [t2:7]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t16, plain, ( rcenter(vd1080, vd1095) ),
% 222.36/222.68 inference(extension, [status(thm), parent(t2:8)], [f_2_4]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t17, plain, $false,
% 222.36/222.68 inference(connection, [status(thm), parent(t16:1)], [t16:1,t2:8]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t18, plain, vd1081 = sK2,
% 222.36/222.68 inference(lemma_extension, [status(thm), parent(t2:9)], [l7:1]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t19, plain, $false,
% 222.36/222.68 inference(connection, [status(thm), parent(t18:1)], [t18:1,t2:9]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t20, plain, ( ron(vd1081, sK1) ),
% 222.36/222.68 inference(extension, [status(thm), parent(t2:10)], [f_1_6]) ).
% 222.36/222.68
% 222.36/222.68 cnf(t21, plain, $false,
% 222.36/222.68 inference(connection, [status(thm), parent(t20:1)], [t20:1,t2:10]) ).
% 222.36/222.68
% 222.36/222.68 % SZS output end Proof for theBenchmark
%------------------------------------------------------------------------------