%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : GEO117+1 : TPTP v9.3.1. Released v2.4.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 : n001.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:39:32 AM UTC 2026
% Result : Theorem 7.66s 7.91s
% Output : Proof 7.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 8
% Syntax : Number of formulae : 60 ( 27 unt; 0 def)
% Number of atoms : 235 ( 30 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 276 ( 101 ~; 96 |; 74 &)
% ( 4 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-5 aty)
% Number of variables : 181 ( 2 sgn 131 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(c3,axiom,
! [C] :
? [P] : inner_point(P,C),
file('GEO004+0.ax',c3) ).
fof(c4,axiom,
! [C,P] :
( inner_point(P,C)
=> ? [C1,C2] :
( C = sum(C1,C2)
& meet(P,C1,C2) ) ),
file('GEO004+0.ax',c4) ).
fof(between_c_defn,axiom,
! [C,P,Q,R] :
( between_c(C,P,Q,R)
<=> ( ? [Cpp] :
( inner_point(Q,Cpp)
& end_point(R,Cpp)
& end_point(P,Cpp)
& part_of(Cpp,C) )
& P != R ) ),
file('GEO004+1.ax',between_c_defn) ).
fof(between_o_defn,axiom,
! [O,P,Q,R] :
( between_o(O,P,Q,R)
<=> ( ( ordered_by(O,Q,P)
& ordered_by(O,R,Q) )
| ( ordered_by(O,Q,R)
& ordered_by(O,P,Q) ) ) ),
file('GEO004+2.ax',between_o_defn) ).
fof(o3,axiom,
! [P,Q,R,O] :
( between_o(O,P,Q,R)
<=> ? [C] :
( between_c(C,P,Q,R)
& ! [P] :
( incident_o(P,O)
<=> incident_c(P,C) ) ) ),
file('GEO004+2.ax',o3) ).
fof(theorem_4_4,conjecture,
! [O,P] : ~ ordered_by(O,P,P),
file('theBenchmark.p',theorem_4_4) ).
fof(f_10_1,plain,
! [C] :
? [P] : inner_point(P,C),
inference(fof_nnf,[status(thm)],[c3]) ).
fof(f_10_2,plain,
! [U_68] :
? [U_67] : inner_point(U_67,U_68),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
! [U_68] : inner_point(sK9(U_68),U_68),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_67,sK9(U_68))],[f_10_2]) ).
cnf(f_10_4,plain,
inner_point(sK9(U_68),U_68),
inference(clausify,[status(thm)],[f_10_3]) ).
fof(f_11_1,plain,
! [C,P] :
( ? [C1,C2] :
( C = sum(C1,C2)
& meet(P,C1,C2) )
| ~ inner_point(P,C) ),
inference(fof_nnf,[status(thm)],[c4]) ).
fof(f_11_2,plain,
! [U_72,U_71] :
( ? [U_70,U_69] :
( U_72 = sum(U_70,U_69)
& meet(U_71,U_70,U_69) )
| ~ inner_point(U_71,U_72) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
! [U_72,U_71] :
( ? [U_69] :
( U_72 = sum(sK10(U_72,U_71),U_69)
& meet(U_71,sK10(U_72,U_71),U_69) )
| ~ inner_point(U_71,U_72) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_70,sK10(U_72,U_71))],[f_11_2]) ).
fof(f_11_4,plain,
! [U_72,U_71] :
( ( U_72 = sum(sK10(U_72,U_71),sK11(U_72,U_71))
& meet(U_71,sK10(U_72,U_71),sK11(U_72,U_71)) )
| ~ inner_point(U_71,U_72) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_69,sK11(U_72,U_71))],[f_11_3]) ).
cnf(f_11_6,plain,
( U_72 = sum(sK10(U_72,U_71),sK11(U_72,U_71))
| ~ inner_point(U_71,U_72) ),
inference(clausify,[status(thm)],[f_11_4]) ).
fof(f_17_1,plain,
! [C,P,Q,R] :
( ( between_c(C,P,Q,R)
| ! [Cpp] :
( ~ inner_point(Q,Cpp)
| ~ end_point(R,Cpp)
| ~ end_point(P,Cpp)
| ~ part_of(Cpp,C) )
| P = R )
& ( ( ? [Cpp] :
( inner_point(Q,Cpp)
& end_point(R,Cpp)
& end_point(P,Cpp)
& part_of(Cpp,C) )
& P != R )
| ~ between_c(C,P,Q,R) ) ),
inference(fof_nnf,[status(thm)],[between_c_defn]) ).
fof(f_17_2,plain,
! [U_99,U_98,U_97,U_96] :
( ( between_c(U_99,U_98,U_97,U_96)
| ! [U_95] :
( ~ inner_point(U_97,U_95)
| ~ end_point(U_96,U_95)
| ~ end_point(U_98,U_95)
| ~ part_of(U_95,U_99) )
| U_98 = U_96 )
& ( ( ? [U_94] :
( inner_point(U_97,U_94)
& end_point(U_96,U_94)
& end_point(U_98,U_94)
& part_of(U_94,U_99) )
& U_98 != U_96 )
| ~ between_c(U_99,U_98,U_97,U_96) ) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
( ! [U_107,U_105,U_103,U_101] :
( between_c(U_107,U_105,U_103,U_101)
| ! [U_95] :
( ~ inner_point(U_103,U_95)
| ~ end_point(U_101,U_95)
| ~ end_point(U_105,U_95)
| ~ part_of(U_95,U_107) )
| U_105 = U_101 )
& ! [U_106,U_104,U_102,U_100] :
( ( ? [U_94] :
( inner_point(U_102,U_94)
& end_point(U_100,U_94)
& end_point(U_104,U_94)
& part_of(U_94,U_106) )
& U_104 != U_100 )
| ~ between_c(U_106,U_104,U_102,U_100) ) ),
inference(miniscope,[status(thm)],[f_17_2]) ).
fof(f_17_4,plain,
( ! [U_107,U_105,U_103,U_101] :
( between_c(U_107,U_105,U_103,U_101)
| ! [U_95] :
( ~ inner_point(U_103,U_95)
| ~ end_point(U_101,U_95)
| ~ end_point(U_105,U_95)
| ~ part_of(U_95,U_107) )
| U_105 = U_101 )
& ! [U_106,U_104,U_102,U_100] :
( ( inner_point(U_102,sK16(U_106,U_104,U_102,U_100))
& end_point(U_100,sK16(U_106,U_104,U_102,U_100))
& end_point(U_104,sK16(U_106,U_104,U_102,U_100))
& part_of(sK16(U_106,U_104,U_102,U_100),U_106)
& U_104 != U_100 )
| ~ between_c(U_106,U_104,U_102,U_100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_94,sK16(U_106,U_104,U_102,U_100))],[f_17_3]) ).
cnf(f_17_5,plain,
( U_104 != U_100
| ~ between_c(U_106,U_104,U_102,U_100) ),
inference(clausify,[status(thm)],[f_17_4]) ).
fof(f_18_1,plain,
! [O,P,Q,R] :
( ( between_o(O,P,Q,R)
| ( ( ~ ordered_by(O,Q,P)
| ~ ordered_by(O,R,Q) )
& ( ~ ordered_by(O,Q,R)
| ~ ordered_by(O,P,Q) ) ) )
& ( ( ordered_by(O,Q,P)
& ordered_by(O,R,Q) )
| ( ordered_by(O,Q,R)
& ordered_by(O,P,Q) )
| ~ between_o(O,P,Q,R) ) ),
inference(fof_nnf,[status(thm)],[between_o_defn]) ).
fof(f_18_2,plain,
! [U_111,U_110,U_109,U_108] :
( ( between_o(U_111,U_110,U_109,U_108)
| ( ( ~ ordered_by(U_111,U_109,U_110)
| ~ ordered_by(U_111,U_108,U_109) )
& ( ~ ordered_by(U_111,U_109,U_108)
| ~ ordered_by(U_111,U_110,U_109) ) ) )
& ( ( ordered_by(U_111,U_109,U_110)
& ordered_by(U_111,U_108,U_109) )
| ( ordered_by(U_111,U_109,U_108)
& ordered_by(U_111,U_110,U_109) )
| ~ between_o(U_111,U_110,U_109,U_108) ) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
( ! [U_119,U_117,U_115,U_113] :
( between_o(U_119,U_117,U_115,U_113)
| ( ( ~ ordered_by(U_119,U_115,U_117)
| ~ ordered_by(U_119,U_113,U_115) )
& ( ~ ordered_by(U_119,U_115,U_113)
| ~ ordered_by(U_119,U_117,U_115) ) ) )
& ! [U_118,U_116,U_114,U_112] :
( ( ordered_by(U_118,U_114,U_116)
& ordered_by(U_118,U_112,U_114) )
| ( ordered_by(U_118,U_114,U_112)
& ordered_by(U_118,U_116,U_114) )
| ~ between_o(U_118,U_116,U_114,U_112) ) ),
inference(miniscope,[status(thm)],[f_18_2]) ).
cnf(f_18_9,plain,
( ~ ordered_by(U_119,U_115,U_117)
| ~ ordered_by(U_119,U_113,U_115)
| between_o(U_119,U_117,U_115,U_113) ),
inference(clausify,[status(thm)],[f_18_3]) ).
fof(f_23_1,plain,
! [P,Q,R,O] :
( ( between_o(O,P,Q,R)
| ! [C] :
( ~ between_c(C,P,Q,R)
| ? [P] :
( ( ~ incident_o(P,O)
& incident_c(P,C) )
| ( ~ incident_c(P,C)
& incident_o(P,O) ) ) ) )
& ( ? [C] :
( between_c(C,P,Q,R)
& ! [P] :
( ( incident_o(P,O)
| ~ incident_c(P,C) )
& ( incident_c(P,C)
| ~ incident_o(P,O) ) ) )
| ~ between_o(O,P,Q,R) ) ),
inference(fof_nnf,[status(thm)],[o3]) ).
fof(f_23_2,plain,
! [U_151,U_150,U_149,U_148] :
( ( between_o(U_148,U_151,U_150,U_149)
| ! [U_147] :
( ~ between_c(U_147,U_151,U_150,U_149)
| ? [U_146] :
( ( ~ incident_o(U_146,U_148)
& incident_c(U_146,U_147) )
| ( ~ incident_c(U_146,U_147)
& incident_o(U_146,U_148) ) ) ) )
& ( ? [U_145] :
( between_c(U_145,U_151,U_150,U_149)
& ! [U_144] :
( ( incident_o(U_144,U_148)
| ~ incident_c(U_144,U_145) )
& ( incident_c(U_144,U_145)
| ~ incident_o(U_144,U_148) ) ) )
| ~ between_o(U_148,U_151,U_150,U_149) ) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
( ! [U_163,U_161,U_159,U_157] :
( between_o(U_157,U_163,U_161,U_159)
| ! [U_147] :
( ~ between_c(U_147,U_163,U_161,U_159)
| ? [U_155] :
( ~ incident_o(U_155,U_157)
& incident_c(U_155,U_147) )
| ? [U_154] :
( ~ incident_c(U_154,U_147)
& incident_o(U_154,U_157) ) ) )
& ! [U_162,U_160,U_158,U_156] :
( ? [U_145] :
( between_c(U_145,U_162,U_160,U_158)
& ! [U_153] :
( incident_o(U_153,U_156)
| ~ incident_c(U_153,U_145) )
& ! [U_152] :
( incident_c(U_152,U_145)
| ~ incident_o(U_152,U_156) ) )
| ~ between_o(U_156,U_162,U_160,U_158) ) ),
inference(miniscope,[status(thm)],[f_23_2]) ).
fof(f_23_4,plain,
( ! [U_163,U_161,U_159,U_157] :
( between_o(U_157,U_163,U_161,U_159)
| ! [U_147] :
( ~ between_c(U_147,U_163,U_161,U_159)
| ? [U_155] :
( ~ incident_o(U_155,U_157)
& incident_c(U_155,U_147) )
| ? [U_154] :
( ~ incident_c(U_154,U_147)
& incident_o(U_154,U_157) ) ) )
& ! [U_162,U_160,U_158,U_156] :
( ( between_c(sK20(U_162,U_160,U_158,U_156),U_162,U_160,U_158)
& ! [U_153] :
( incident_o(U_153,U_156)
| ~ incident_c(U_153,sK20(U_162,U_160,U_158,U_156)) )
& ! [U_152] :
( incident_c(U_152,sK20(U_162,U_160,U_158,U_156))
| ~ incident_o(U_152,U_156) ) )
| ~ between_o(U_156,U_162,U_160,U_158) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_145,sK20(U_162,U_160,U_158,U_156))],[f_23_3]) ).
fof(f_23_5,plain,
( ! [U_163,U_161,U_159,U_157] :
( between_o(U_157,U_163,U_161,U_159)
| ! [U_147] :
( ~ between_c(U_147,U_163,U_161,U_159)
| ? [U_155] :
( ~ incident_o(U_155,U_157)
& incident_c(U_155,U_147) )
| ( ~ incident_c(sK21(U_163,U_161,U_159,U_157,U_147),U_147)
& incident_o(sK21(U_163,U_161,U_159,U_157,U_147),U_157) ) ) )
& ! [U_162,U_160,U_158,U_156] :
( ( between_c(sK20(U_162,U_160,U_158,U_156),U_162,U_160,U_158)
& ! [U_153] :
( incident_o(U_153,U_156)
| ~ incident_c(U_153,sK20(U_162,U_160,U_158,U_156)) )
& ! [U_152] :
( incident_c(U_152,sK20(U_162,U_160,U_158,U_156))
| ~ incident_o(U_152,U_156) ) )
| ~ between_o(U_156,U_162,U_160,U_158) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_154,sK21(U_163,U_161,U_159,U_157,U_147))],[f_23_4]) ).
fof(f_23_6,plain,
( ! [U_163,U_161,U_159,U_157] :
( between_o(U_157,U_163,U_161,U_159)
| ! [U_147] :
( ~ between_c(U_147,U_163,U_161,U_159)
| ( ~ incident_o(sK22(U_163,U_161,U_159,U_157,U_147),U_157)
& incident_c(sK22(U_163,U_161,U_159,U_157,U_147),U_147) )
| ( ~ incident_c(sK21(U_163,U_161,U_159,U_157,U_147),U_147)
& incident_o(sK21(U_163,U_161,U_159,U_157,U_147),U_157) ) ) )
& ! [U_162,U_160,U_158,U_156] :
( ( between_c(sK20(U_162,U_160,U_158,U_156),U_162,U_160,U_158)
& ! [U_153] :
( incident_o(U_153,U_156)
| ~ incident_c(U_153,sK20(U_162,U_160,U_158,U_156)) )
& ! [U_152] :
( incident_c(U_152,sK20(U_162,U_160,U_158,U_156))
| ~ incident_o(U_152,U_156) ) )
| ~ between_o(U_156,U_162,U_160,U_158) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_155,sK22(U_163,U_161,U_159,U_157,U_147))],[f_23_5]) ).
cnf(f_23_9,plain,
( between_c(sK20(U_162,U_160,U_158,U_156),U_162,U_160,U_158)
| ~ between_o(U_156,U_162,U_160,U_158) ),
inference(clausify,[status(thm)],[f_23_6]) ).
fof(f_28_1,negated_conjecture,
~ ! [O,P] : ~ ordered_by(O,P,P),
inference(negate,[status(cth)],[theorem_4_4]) ).
fof(f_28_2,negated_conjecture,
? [O,P] : ordered_by(O,P,P),
inference(fof_nnf,[status(thm)],[f_28_1]) ).
fof(f_28_3,negated_conjecture,
? [U_194,U_193] : ordered_by(U_194,U_193,U_193),
inference(variable_rename,[status(thm)],[f_28_2]) ).
fof(f_28_4,negated_conjecture,
? [U_193] : ordered_by(sK31,U_193,U_193),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31]),skolemize(U_194,sK31)],[f_28_3]) ).
fof(f_28_5,negated_conjecture,
ordered_by(sK31,sK32,sK32),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(U_193,sK32)],[f_28_4]) ).
fof(f_28_6,negated_conjecture,
ordered_by(sK31,sK32,sK32),
inference(definitional_conversion,[status(esa)],[f_28_5]) ).
cnf(f_28_7,negated_conjecture,
ordered_by(sK31,sK32,sK32),
inference(clausify,[status(thm)],[f_28_6]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(t1,plain,
( sK32 != sK32
| ~ between_c(sK20(sK32,sK32,sK32,sK31),sK32,sK32,sK32) ),
inference(start,[status(thm),parent(0:0)],[f_17_5]) ).
cnf(t2,plain,
( ~ between_o(sK31,sK32,sK32,sK32)
| between_c(sK20(sK32,sK32,sK32,sK31),sK32,sK32,sK32) ),
inference(extension,[status(thm),parent(t1:1)],[f_23_9]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ ordered_by(sK31,sK32,sK32)
| ~ ordered_by(sK31,sK32,sK32)
| between_o(sK31,sK32,sK32,sK32) ),
inference(extension,[status(thm),parent(t2:2)],[f_18_9]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
ordered_by(sK31,sK32,sK32),
inference(extension,[status(thm),parent(t4:2)],[f_28_7]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
ordered_by(sK31,sK32,sK32),
inference(extension,[status(thm),parent(t4:3)],[f_28_7]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t4:3]) ).
cnf(t10,plain,
( sum(sK10(sK32,sK9(sK32)),sK11(sK32,sK9(sK32))) != sK32
| sK32 != sum(sK10(sK32,sK9(sK32)),sK11(sK32,sK9(sK32)))
| sK32 = sK32 ),
inference(extension,[status(thm),parent(t1:2)],[equality_3]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t1:2]) ).
cnf(t12,plain,
( ~ inner_point(sK9(sK32),sK32)
| sK32 = sum(sK10(sK32,sK9(sK32)),sK11(sK32,sK9(sK32))) ),
inference(extension,[status(thm),parent(t10:2)],[f_11_6]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
inner_point(sK9(sK32),sK32),
inference(extension,[status(thm),parent(t12:2)],[f_10_4]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(l6,lemma,
sK32 = sum(sK10(sK32,sK9(sK32)),sK11(sK32,sK9(sK32))),
inference(lemma,[status(cth),parent(t10:2),below(t1:2)],[t10:2]) ).
cnf(t16,plain,
( sK32 != sum(sK10(sK32,sK9(sK32)),sK11(sK32,sK9(sK32)))
| sum(sK10(sK32,sK9(sK32)),sK11(sK32,sK9(sK32))) = sK32 ),
inference(extension,[status(thm),parent(t10:3)],[equality_2]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t10:3]) ).
cnf(t18,plain,
sK32 = sum(sK10(sK32,sK9(sK32)),sK11(sK32,sK9(sK32))),
inference(lemma_extension,[status(thm),parent(t16:2)],[l6:1]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t16:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO117+1 : TPTP v9.3.1. Released v2.4.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.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 19 07:34:08 UTC 2026
% 0.09/0.37 % CPUTime :
% 7.66/7.91 % SZS status Theorem for theBenchmark
% 7.66/7.91 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------