%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO297+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 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 : Fri Sep 25 01:20:55 PM UTC 2026
% Result : Theorem 64.82s 14.32s
% Output : CNFRefutation 64.82s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f163ERROR: Could not build tree for root c_62605ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f33,axiom,
? [X0] :
( rpoint(X0)
& vd1199 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(s1(plural(271)))') ).
fof(f34,axiom,
~ ron(vd1187,vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','neg(neg(270))') ).
fof(f164,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rline(X7)
| X6 != X7
| X0 = X2
| X0 = X4
| ~ ron(X0,X6)
| ~ ron(X2,X6)
| ( ( ron(X4,X6)
& ~ rR(X0,X2,X4) )
<=> vangle(X2,X0,X4) = v0 ) ),
inference(flattening,[],[f163]) ).
fof(f171,plain,
( ? [X6] :
( rpoint(X6)
& vd1178 = X6 )
& ? [X5] :
( rpoint(X5)
& vd1179 = X5 )
& ? [X4] :
( rpoint(X4)
& vd1180 = X4 )
& vd1178 != vd1179
& vd1178 != vd1180
& vd1179 != vd1180
& ? [X3] :
( rpoint(X3)
& vd1185 = X3 )
& ? [X2] :
( rpoint(X2)
& vd1186 = X2 )
& ? [X1] :
( rpoint(X1)
& vd1187 = X1 )
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& ! [X0] :
( ~ rline(X0)
| ~ ron(vd1185,X0)
| ~ ron(vd1186,X0)
| ~ ron(vd1187,X0) ) ),
inference(ennf_transformation,[],[f20]) ).
fof(f202,plain,
! [X0,X1,X2,X3] :
( ! [X5] :
( ~ rpoint(X5)
| X0 != X5 )
| ! [X4] :
( ~ rpoint(X4)
| X1 != X4 )
| ~ rline(X3)
| X2 != X3
| ~ rS(X0,X1,X2)
| ~ ron(X0,X2) ),
inference(ennf_transformation,[],[f66]) ).
fof(f203,plain,
! [X0,X1,X2,X3] :
( ! [X5] :
( ~ rpoint(X5)
| X0 != X5 )
| ! [X4] :
( ~ rpoint(X4)
| X1 != X4 )
| ~ rline(X3)
| X2 != X3
| ~ rS(X0,X1,X2)
| ~ ron(X0,X2) ),
inference(flattening,[],[f202]) ).
fof(f258,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ! [X13] :
( ~ rline(X13)
| X0 != X13 )
| ! [X12] :
( ~ rline(X12)
| X1 != X12 )
| ! [X11] :
( ~ rline(X11)
| X2 != X11 )
| ! [X10] :
( ~ rpoint(X10)
| X3 != X10 )
| ! [X9] :
( ~ rpoint(X9)
| X4 != X9 )
| ! [X8] :
( ~ rpoint(X8)
| X5 != X8 )
| ! [X7] :
( ~ rpoint(X7)
| X6 != X7 )
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X3,X2)
| ~ ron(X4,X0)
| ~ ron(X5,X2)
| ~ ron(X6,X2)
| ~ rS(X5,X6,X0)
| ~ rS(X4,X5,X2)
| ~ rS(X4,X6,X1) ),
inference(ennf_transformation,[],[f94]) ).
fof(f259,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ! [X13] :
( ~ rline(X13)
| X0 != X13 )
| ! [X12] :
( ~ rline(X12)
| X1 != X12 )
| ! [X11] :
( ~ rline(X11)
| X2 != X11 )
| ! [X10] :
( ~ rpoint(X10)
| X3 != X10 )
| ! [X9] :
( ~ rpoint(X9)
| X4 != X9 )
| ! [X8] :
( ~ rpoint(X8)
| X5 != X8 )
| ! [X7] :
( ~ rpoint(X7)
| X6 != X7 )
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X3,X2)
| ~ ron(X4,X0)
| ~ ron(X5,X2)
| ~ ron(X6,X2)
| ~ rS(X5,X6,X0)
| ~ rS(X4,X5,X2)
| ~ rS(X4,X6,X1) ),
inference(flattening,[],[f258]) ).
fof(f272,plain,
! [X0,X1,X2,X3] :
( ~ rpoint(X1)
| X0 != X1
| ~ rline(X3)
| X2 != X3
| ron(X0,X2)
| rS(X0,X0,X2) ),
inference(ennf_transformation,[],[f101]) ).
fof(f273,plain,
! [X0,X1,X2,X3] :
( ~ rpoint(X1)
| X0 != X1
| ~ rline(X3)
| X2 != X3
| ron(X0,X2)
| rS(X0,X0,X2) ),
inference(flattening,[],[f272]) ).
fof(f376,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rline(X7)
| X6 != X7
| X0 = X2
| X0 = X4
| ~ ron(X0,X6)
| ~ ron(X2,X6)
| ( ( ~ ron(X4,X6)
| rR(X0,X2,X4)
| vangle(X2,X0,X4) = v0 )
& ( v0 != vangle(X2,X0,X4)
| ( ron(X4,X6)
& ~ rR(X0,X2,X4) ) ) ) ),
inference(nnf_transformation,[],[f164]) ).
fof(f377,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rline(X7)
| X6 != X7
| X0 = X2
| X0 = X4
| ~ ron(X0,X6)
| ~ ron(X2,X6)
| ( ( ~ ron(X4,X6)
| rR(X0,X2,X4)
| vangle(X2,X0,X4) = v0 )
& ( v0 != vangle(X2,X0,X4)
| ( ron(X4,X6)
& ~ rR(X0,X2,X4) ) ) ) ),
inference(flattening,[],[f376]) ).
fof(f378,plain,
( rpoint(sK6)
& vd1178 = sK6
& rpoint(sK5)
& vd1179 = sK5
& rpoint(sK4)
& vd1180 = sK4
& vd1178 != vd1179
& vd1178 != vd1180
& vd1179 != vd1180
& rpoint(sK3)
& vd1185 = sK3
& rpoint(sK2)
& vd1186 = sK2
& rpoint(sK1)
& vd1187 = sK1
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& ! [X0] :
( ~ rline(X0)
| ~ ron(vd1185,X0)
| ~ ron(vd1186,X0)
| ~ ron(vd1187,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6]),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6)],[f171]) ).
fof(f379,plain,
( rpoint(sK7)
& vd1201 = sK7 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X0,sK7)],[f31]) ).
fof(f381,plain,
( rpoint(sK9)
& vd1199 = sK9 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X0,sK9)],[f33]) ).
fof(f453,plain,
vangle(vd1187,vd1185,vd1201) = v0,
inference(cnf_transformation,[],[f4]) ).
fof(f454,plain,
ron(vd1187,vd1232),
inference(cnf_transformation,[],[f5]) ).
fof(f457,plain,
ron(vd1185,vd1232),
inference(cnf_transformation,[],[f8]) ).
fof(f458,plain,
rline(vd1232),
inference(cnf_transformation,[],[f9]) ).
fof(f460,plain,
vd1185 = vd1199,
inference(cnf_transformation,[],[f11]) ).
fof(f463,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rline(X7)
| X6 != X7
| X0 = X2
| X0 = X4
| ~ ron(X0,X6)
| ~ ron(X2,X6)
| v0 != vangle(X2,X0,X4)
| ron(X4,X6) ),
inference(cnf_transformation,[],[f377]) ).
fof(f484,plain,
rpoint(sK1),
inference(cnf_transformation,[],[f378]) ).
fof(f485,plain,
vd1187 = sK1,
inference(cnf_transformation,[],[f378]) ).
fof(f492,plain,
rS(vd1201,vd1187,vd1197),
inference(cnf_transformation,[],[f23]) ).
fof(f500,plain,
rpoint(sK7),
inference(cnf_transformation,[],[f379]) ).
fof(f501,plain,
vd1201 = sK7,
inference(cnf_transformation,[],[f379]) ).
fof(f504,plain,
rpoint(sK9),
inference(cnf_transformation,[],[f381]) ).
fof(f505,plain,
vd1199 = sK9,
inference(cnf_transformation,[],[f381]) ).
fof(f506,plain,
~ ron(vd1187,vd1197),
inference(cnf_transformation,[],[f34]) ).
fof(f515,plain,
rline(vd1197),
inference(cnf_transformation,[],[f41]) ).
fof(f522,plain,
ron(vd1199,vd1197),
inference(cnf_transformation,[],[f48]) ).
fof(f528,plain,
~ ron(vd1201,vd1232),
inference(cnf_transformation,[],[f51]) ).
fof(f544,plain,
v0 = vd684,
inference(cnf_transformation,[],[f64]) ).
fof(f546,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rline(X3)
| X2 != X3
| ~ rS(X0,X1,X2)
| ~ ron(X0,X2) ),
inference(cnf_transformation,[],[f203]) ).
fof(f599,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ rline(X13)
| X0 != X13
| ~ rline(X12)
| X1 != X12
| ~ rline(X11)
| X2 != X11
| ~ rpoint(X10)
| X3 != X10
| ~ rpoint(X9)
| X4 != X9
| ~ rpoint(X8)
| X5 != X8
| ~ rpoint(X7)
| X6 != X7
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X3,X2)
| ~ ron(X4,X0)
| ~ ron(X5,X2)
| ~ ron(X6,X2)
| ~ rS(X5,X6,X0)
| ~ rS(X4,X5,X2)
| ~ rS(X4,X6,X1) ),
inference(cnf_transformation,[],[f259]) ).
fof(f606,plain,
! [X2,X3,X0,X1] :
( ~ rpoint(X1)
| X0 != X1
| ~ rline(X3)
| X2 != X3
| ron(X0,X2)
| rS(X0,X0,X2) ),
inference(cnf_transformation,[],[f273]) ).
fof(f751,plain,
vd1185 = sK9,
inference(definition_unfolding,[],[f460,f505]) ).
fof(f754,plain,
vd684 = vangle(sK1,sK9,sK7),
inference(definition_unfolding,[],[f453,f485,f751,f501,f544]) ).
fof(f755,plain,
ron(sK1,vd1232),
inference(definition_unfolding,[],[f454,f485]) ).
fof(f758,plain,
ron(sK9,vd1232),
inference(definition_unfolding,[],[f457,f751]) ).
fof(f761,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rline(X7)
| X6 != X7
| X0 = X2
| X0 = X4
| ~ ron(X0,X6)
| ~ ron(X2,X6)
| vangle(X2,X0,X4) != vd684
| ron(X4,X6) ),
inference(definition_unfolding,[],[f463,f544]) ).
fof(f779,plain,
rS(sK7,sK1,vd1197),
inference(definition_unfolding,[],[f492,f501,f485]) ).
fof(f788,plain,
~ ron(sK1,vd1197),
inference(definition_unfolding,[],[f506,f485]) ).
fof(f799,plain,
ron(sK9,vd1197),
inference(definition_unfolding,[],[f522,f505]) ).
fof(f800,plain,
~ ron(sK7,vd1232),
inference(definition_unfolding,[],[f528,f501]) ).
fof(f811,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rline(X7)
| X0 = X2
| X0 = X4
| ~ ron(X0,X7)
| ~ ron(X2,X7)
| vangle(X2,X0,X4) != vd684
| ron(X4,X7) ),
inference(equality_resolution,[],[f761]) ).
fof(f812,plain,
! [X2,X3,X0,X1,X7,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| ~ rline(X7)
| X0 = X2
| X0 = X5
| ~ ron(X0,X7)
| ~ ron(X2,X7)
| vd684 != vangle(X2,X0,X5)
| ron(X5,X7) ),
inference(equality_resolution,[],[f811]) ).
fof(f813,plain,
! [X3,X0,X1,X7,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rline(X7)
| X0 = X3
| X0 = X5
| ~ ron(X0,X7)
| ~ ron(X3,X7)
| vd684 != vangle(X3,X0,X5)
| ron(X5,X7) ),
inference(equality_resolution,[],[f812]) ).
fof(f814,plain,
! [X3,X1,X7,X5] :
( ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rline(X7)
| X1 = X3
| X1 = X5
| ~ ron(X1,X7)
| ~ ron(X3,X7)
| vd684 != vangle(X3,X1,X5)
| ron(X5,X7) ),
inference(equality_resolution,[],[f813]) ).
fof(f887,plain,
! [X3,X0,X1,X4,X5] :
( ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rline(X3)
| ~ rS(X0,X1,X3)
| ~ ron(X0,X3) ),
inference(equality_resolution,[],[f546]) ).
fof(f888,plain,
! [X3,X0,X4,X5] :
( ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| ~ rline(X3)
| ~ rS(X0,X4,X3)
| ~ ron(X0,X3) ),
inference(equality_resolution,[],[f887]) ).
fof(f889,plain,
! [X3,X4,X5] :
( ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rline(X3)
| ~ rS(X5,X4,X3)
| ~ ron(X5,X3) ),
inference(equality_resolution,[],[f888]) ).
fof(f1065,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X5,X12,X13] :
( ~ rline(X13)
| X0 != X13
| ~ rline(X12)
| X1 != X12
| ~ rline(X11)
| X2 != X11
| ~ rpoint(X10)
| X3 != X10
| ~ rpoint(X9)
| X4 != X9
| ~ rpoint(X8)
| X5 != X8
| ~ rpoint(X7)
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X3,X2)
| ~ ron(X4,X0)
| ~ ron(X5,X2)
| ~ ron(X7,X2)
| ~ rS(X5,X7,X0)
| ~ rS(X4,X5,X2)
| ~ rS(X4,X7,X1) ),
inference(equality_resolution,[],[f599]) ).
fof(f1066,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X12,X13] :
( ~ rline(X13)
| X0 != X13
| ~ rline(X12)
| X1 != X12
| ~ rline(X11)
| X2 != X11
| ~ rpoint(X10)
| X3 != X10
| ~ rpoint(X9)
| X4 != X9
| ~ rpoint(X8)
| ~ rpoint(X7)
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X3,X2)
| ~ ron(X4,X0)
| ~ ron(X8,X2)
| ~ ron(X7,X2)
| ~ rS(X8,X7,X0)
| ~ rS(X4,X8,X2)
| ~ rS(X4,X7,X1) ),
inference(equality_resolution,[],[f1065]) ).
fof(f1067,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X12,X13] :
( ~ rline(X13)
| X0 != X13
| ~ rline(X12)
| X1 != X12
| ~ rline(X11)
| X2 != X11
| ~ rpoint(X10)
| X3 != X10
| ~ rpoint(X9)
| ~ rpoint(X8)
| ~ rpoint(X7)
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X3,X2)
| ~ ron(X9,X0)
| ~ ron(X8,X2)
| ~ ron(X7,X2)
| ~ rS(X8,X7,X0)
| ~ rS(X9,X8,X2)
| ~ rS(X9,X7,X1) ),
inference(equality_resolution,[],[f1066]) ).
fof(f1068,plain,
! [X2,X10,X0,X11,X1,X8,X9,X7,X12,X13] :
( ~ rline(X13)
| X0 != X13
| ~ rline(X12)
| X1 != X12
| ~ rline(X11)
| X2 != X11
| ~ rpoint(X10)
| ~ rpoint(X9)
| ~ rpoint(X8)
| ~ rpoint(X7)
| ~ ron(X10,X0)
| ~ ron(X10,X1)
| ~ ron(X10,X2)
| ~ ron(X9,X0)
| ~ ron(X8,X2)
| ~ ron(X7,X2)
| ~ rS(X8,X7,X0)
| ~ rS(X9,X8,X2)
| ~ rS(X9,X7,X1) ),
inference(equality_resolution,[],[f1067]) ).
fof(f1069,plain,
! [X10,X0,X11,X1,X8,X9,X7,X12,X13] :
( ~ rline(X13)
| X0 != X13
| ~ rline(X12)
| X1 != X12
| ~ rline(X11)
| ~ rpoint(X10)
| ~ rpoint(X9)
| ~ rpoint(X8)
| ~ rpoint(X7)
| ~ ron(X10,X0)
| ~ ron(X10,X1)
| ~ ron(X10,X11)
| ~ ron(X9,X0)
| ~ ron(X8,X11)
| ~ ron(X7,X11)
| ~ rS(X8,X7,X0)
| ~ rS(X9,X8,X11)
| ~ rS(X9,X7,X1) ),
inference(equality_resolution,[],[f1068]) ).
fof(f1070,plain,
! [X10,X0,X11,X8,X9,X7,X12,X13] :
( ~ rline(X13)
| X0 != X13
| ~ rline(X12)
| ~ rline(X11)
| ~ rpoint(X10)
| ~ rpoint(X9)
| ~ rpoint(X8)
| ~ rpoint(X7)
| ~ ron(X10,X0)
| ~ ron(X10,X12)
| ~ ron(X10,X11)
| ~ ron(X9,X0)
| ~ ron(X8,X11)
| ~ ron(X7,X11)
| ~ rS(X8,X7,X0)
| ~ rS(X9,X8,X11)
| ~ rS(X9,X7,X12) ),
inference(equality_resolution,[],[f1069]) ).
fof(f1071,plain,
! [X10,X11,X8,X9,X7,X12,X13] :
( ~ rline(X13)
| ~ rline(X12)
| ~ rline(X11)
| ~ rpoint(X10)
| ~ rpoint(X9)
| ~ rpoint(X8)
| ~ rpoint(X7)
| ~ ron(X10,X13)
| ~ ron(X10,X12)
| ~ ron(X10,X11)
| ~ ron(X9,X13)
| ~ ron(X8,X11)
| ~ ron(X7,X11)
| ~ rS(X8,X7,X13)
| ~ rS(X9,X8,X11)
| ~ rS(X9,X7,X12) ),
inference(equality_resolution,[],[f1070]) ).
fof(f1097,plain,
! [X3,X0,X1] :
( ~ rpoint(X1)
| X0 != X1
| ~ rline(X3)
| ron(X0,X3)
| rS(X0,X0,X3) ),
inference(equality_resolution,[],[f606]) ).
fof(f1098,plain,
! [X3,X1] :
( ~ rpoint(X1)
| ~ rline(X3)
| ron(X1,X3)
| rS(X1,X1,X3) ),
inference(equality_resolution,[],[f1097]) ).
tcf(c_50,plain,
vangle(sK1,sK9,sK7) = vd684,
inference(cnf_transformation,[],[f754]) ).
tcf(c_51,plain,
ron(sK1,vd1232),
inference(cnf_transformation,[],[f755]) ).
tcf(c_54,plain,
ron(sK9,vd1232),
inference(cnf_transformation,[],[f758]) ).
tcf(c_55,plain,
rline(vd1232),
inference(cnf_transformation,[],[f458]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ron(X2,X3)
| ( X1 = X2 )
| ( X0 = X1 )
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rline(X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ( vangle(X0,X1,X2) != vd684 ) ),
inference(cnf_transformation,[],[f814]) ).
tcf(c_67,plain,
rpoint(sK1),
inference(cnf_transformation,[],[f484]) ).
tcf(c_79,plain,
rS(sK7,sK1,vd1197),
inference(cnf_transformation,[],[f779]) ).
tcf(c_87,plain,
rpoint(sK7),
inference(cnf_transformation,[],[f500]) ).
tcf(c_90,plain,
rpoint(sK9),
inference(cnf_transformation,[],[f504]) ).
tcf(c_91,plain,
~ ron(sK1,vd1197),
inference(cnf_transformation,[],[f788]) ).
tcf(c_100,plain,
rline(vd1197),
inference(cnf_transformation,[],[f515]) ).
tcf(c_106,plain,
ron(sK9,vd1197),
inference(cnf_transformation,[],[f799]) ).
tcf(c_112,plain,
~ ron(sK7,vd1232),
inference(cnf_transformation,[],[f800]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rline(X2)
| ~ ron(X0,X2)
| ~ rS(X0,X1,X2) ),
inference(cnf_transformation,[],[f889]) ).
tcf(c_182,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ~ rpoint(X6)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rline(X5)
| ~ rline(X4)
| ~ rline(X2)
| ~ ron(X6,X5)
| ~ ron(X6,X4)
| ~ ron(X6,X2)
| ~ ron(X3,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X5)
| ~ rS(X3,X1,X5)
| ~ rS(X0,X3,X4)
| ~ rS(X0,X1,X2) ),
inference(cnf_transformation,[],[f1071]) ).
tcf(c_189,plain,
! [X0: $i,X1: $i] :
( ron(X1,X0)
| rS(X1,X1,X0)
| ~ rpoint(X1)
| ~ rline(X0) ),
inference(cnf_transformation,[],[f1098]) ).
tcf(c_670,plain,
! [X0_iProver_vangle_3: iProver_vangle_3,X0_iProver_sK49_2: iProver_sK49_2] :
( ron(X0_iProver_vangle_3,X0_iProver_sK49_2)
| rS(X0_iProver_vangle_3,X0_iProver_vangle_3,X0_iProver_sK49_2)
| ~ rpoint(X0_iProver_vangle_3)
| ~ rline(X0_iProver_sK49_2) ),
inference(subtyping,[status(esa)],[c_189]) ).
tcf(c_677,plain,
! [X0_iProver_vangle_3: iProver_vangle_3,X0_iProver_sK49_2: iProver_sK49_2,X1_iProver_vangle_3: iProver_vangle_3,X1_iProver_sK49_2: iProver_sK49_2,X2_iProver_vangle_3: iProver_vangle_3,X2_iProver_sK49_2: iProver_sK49_2,X3_iProver_vangle_3: iProver_vangle_3] :
( ~ rpoint(X3_iProver_vangle_3)
| ~ rpoint(X2_iProver_vangle_3)
| ~ rpoint(X1_iProver_vangle_3)
| ~ rpoint(X0_iProver_vangle_3)
| ~ rline(X2_iProver_sK49_2)
| ~ rline(X1_iProver_sK49_2)
| ~ rline(X0_iProver_sK49_2)
| ~ ron(X3_iProver_vangle_3,X2_iProver_sK49_2)
| ~ ron(X3_iProver_vangle_3,X1_iProver_sK49_2)
| ~ ron(X3_iProver_vangle_3,X0_iProver_sK49_2)
| ~ ron(X2_iProver_vangle_3,X0_iProver_sK49_2)
| ~ ron(X1_iProver_vangle_3,X0_iProver_sK49_2)
| ~ ron(X0_iProver_vangle_3,X2_iProver_sK49_2)
| ~ rS(X1_iProver_vangle_3,X2_iProver_vangle_3,X2_iProver_sK49_2)
| ~ rS(X0_iProver_vangle_3,X2_iProver_vangle_3,X1_iProver_sK49_2)
| ~ rS(X0_iProver_vangle_3,X1_iProver_vangle_3,X0_iProver_sK49_2) ),
inference(subtyping,[status(esa)],[c_182]) ).
tcf(c_726,plain,
! [X0_iProver_vangle_3: iProver_vangle_3,X0_iProver_sK49_2: iProver_sK49_2,X1_iProver_vangle_3: iProver_vangle_3] :
( ~ rpoint(X1_iProver_vangle_3)
| ~ rpoint(X0_iProver_vangle_3)
| ~ rline(X0_iProver_sK49_2)
| ~ ron(X0_iProver_vangle_3,X0_iProver_sK49_2)
| ~ rS(X0_iProver_vangle_3,X1_iProver_vangle_3,X0_iProver_sK49_2) ),
inference(subtyping,[status(esa)],[c_129]) ).
tcf(c_788,plain,
! [X0_iProver_vangle_3: iProver_vangle_3,X0_iProver_sK49_2: iProver_sK49_2,X1_iProver_vangle_3: iProver_vangle_3,X2_iProver_vangle_3: iProver_vangle_3] :
( ron(X2_iProver_vangle_3,X0_iProver_sK49_2)
| ( X1_iProver_vangle_3 = X2_iProver_vangle_3 )
| ( X0_iProver_vangle_3 = X1_iProver_vangle_3 )
| ~ rpoint(X2_iProver_vangle_3)
| ~ rpoint(X1_iProver_vangle_3)
| ~ rpoint(X0_iProver_vangle_3)
| ~ rline(X0_iProver_sK49_2)
| ~ ron(X1_iProver_vangle_3,X0_iProver_sK49_2)
| ~ ron(X0_iProver_vangle_3,X0_iProver_sK49_2)
| ( vangle(X0_iProver_vangle_3,X1_iProver_vangle_3,X2_iProver_vangle_3) != vd684 ) ),
inference(subtyping,[status(esa)],[c_58]) ).
tcf(c_794,plain,
vangle(sK1,sK9,sK7) = vd684,
inference(subtyping,[status(esa)],[c_50]) ).
tcf(c_799,plain,
! [X0_iProver_sK49_2: iProver_sK49_2] : X0_iProver_sK49_2 = X0_iProver_sK49_2,
theory(equality) ).
tcf(c_803,plain,
! [X0_iProver_vangle_3: iProver_vangle_3,X0_iProver_sK49_2: iProver_sK49_2,X1_iProver_vangle_3: iProver_vangle_3,X1_iProver_sK49_2: iProver_sK49_2] :
( ron(X0_iProver_vangle_3,X0_iProver_sK49_2)
| ~ ron(X1_iProver_vangle_3,X1_iProver_sK49_2)
| ( X0_iProver_sK49_2 != X1_iProver_sK49_2 )
| ( X0_iProver_vangle_3 != X1_iProver_vangle_3 ) ),
theory(equality) ).
tcf(c_810,plain,
! [X0_iProver_vangle_3: iProver_vangle_3,X0_iProver_sK49_2: iProver_sK49_2,X1_iProver_vangle_3: iProver_vangle_3,X1_iProver_sK49_2: iProver_sK49_2,X2_iProver_vangle_3: iProver_vangle_3,X3_iProver_vangle_3: iProver_vangle_3] :
( rS(X0_iProver_vangle_3,X2_iProver_vangle_3,X0_iProver_sK49_2)
| ~ rS(X1_iProver_vangle_3,X3_iProver_vangle_3,X1_iProver_sK49_2)
| ( X2_iProver_vangle_3 != X3_iProver_vangle_3 )
| ( X0_iProver_sK49_2 != X1_iProver_sK49_2 )
| ( X0_iProver_vangle_3 != X1_iProver_vangle_3 ) ),
theory(equality) ).
tcf(c_823,plain,
vd1197 = vd1197,
inference(instantiation,[status(thm)],[c_799]) ).
tcf(c_896,plain,
( ~ rpoint(sK9)
| ~ rline(vd1197)
| ~ ron(sK9,vd1197)
| ~ rS(sK9,sK9,vd1197) ),
inference(instantiation,[status(thm)],[c_677]) ).
tcf(c_1006,plain,
! [X0_iProver_vangle_3: iProver_vangle_3,X0_iProver_sK49_2: iProver_sK49_2] :
( ron(sK1,vd1197)
| ~ ron(X0_iProver_vangle_3,X0_iProver_sK49_2)
| ( vd1197 != X0_iProver_sK49_2 )
| ( sK1 != X0_iProver_vangle_3 ) ),
inference(instantiation,[status(thm)],[c_803]) ).
tcf(c_1007,plain,
( ron(sK1,vd1197)
| ~ ron(sK9,vd1197)
| ( vd1197 != vd1197 )
| ( sK1 != sK9 ) ),
inference(instantiation,[status(thm)],[c_1006]) ).
tcf(c_1139,plain,
( ~ rpoint(sK7)
| ~ rpoint(sK1)
| ~ rline(vd1197)
| ~ ron(sK7,vd1197)
| ~ rS(sK7,sK1,vd1197) ),
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_3107,plain,
( ron(sK7,vd1197)
| rS(sK7,sK7,vd1197)
| ~ rpoint(sK7)
| ~ rline(vd1197) ),
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_7327,plain,
! [X0_iProver_vangle_3: iProver_vangle_3,X0_iProver_sK49_2: iProver_sK49_2,X1_iProver_vangle_3: iProver_vangle_3] :
( rS(X0_iProver_vangle_3,X1_iProver_vangle_3,X0_iProver_sK49_2)
| ~ rS(sK7,sK7,vd1197)
| ( X1_iProver_vangle_3 != sK7 )
| ( X0_iProver_sK49_2 != vd1197 )
| ( X0_iProver_vangle_3 != sK7 ) ),
inference(instantiation,[status(thm)],[c_810]) ).
tcf(c_7328,plain,
( rS(sK9,sK9,vd1197)
| ~ rS(sK7,sK7,vd1197)
| ( vd1197 != vd1197 )
| ( sK9 != sK7 ) ),
inference(instantiation,[status(thm)],[c_7327]) ).
tcf(c_60340,plain,
! [X0_iProver_vangle_3: iProver_vangle_3,X1_iProver_vangle_3: iProver_vangle_3] :
( ron(sK7,vd1232)
| ( X1_iProver_vangle_3 = sK7 )
| ( X0_iProver_vangle_3 = X1_iProver_vangle_3 )
| ~ rpoint(sK7)
| ~ rline(vd1232)
| ~ rpoint(X1_iProver_vangle_3)
| ~ rpoint(X0_iProver_vangle_3)
| ~ ron(X1_iProver_vangle_3,vd1232)
| ~ ron(X0_iProver_vangle_3,vd1232)
| ( vangle(X0_iProver_vangle_3,X1_iProver_vangle_3,sK7) != vd684 ) ),
inference(instantiation,[status(thm)],[c_788]) ).
tcf(c_62604,plain,
( ron(sK7,vd1232)
| ( sK9 = sK7 )
| ( sK1 = sK9 )
| ~ rpoint(sK7)
| ~ rpoint(sK9)
| ~ rpoint(sK1)
| ~ rline(vd1232)
| ~ ron(sK9,vd1232)
| ~ ron(sK1,vd1232)
| ( vangle(sK1,sK9,sK7) != vd684 ) ),
inference(instantiation,[status(thm)],[c_60340]) ).
tcf(c_62605,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_62604,c_7328,c_3107,c_1139,c_1007,c_794,c_896,c_823,c_79,c_91,c_112,c_51,c_54,c_106,c_55,c_67,c_87,c_90,c_100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO297+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.37 % Computer : n001.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.38 % CPULimit : 300
% 0.08/0.38 % WCLimit : 300
% 0.08/0.38 % DateTime : Wed Sep 23 11:56:36 UTC 2026
% 0.08/0.38 % CPUTime :
% 0.08/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.42 Running first-order theorem proving
% 0.08/0.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.43
% 0.08/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.08/0.43
% 0.08/0.43 % Detected problem language: tptp
% 0.08/0.44 % Proving...
% 64.82/14.32 % SZS status Started for theBenchmark.p
% 64.82/14.32 % SZS status Theorem for theBenchmark.p
% 64.82/14.32
% 64.82/14.32 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 64.82/14.32
% 64.82/14.32 % ------ iProver source info
% 64.82/14.32
% 64.82/14.32 % git: date: 2026-07-19 20:42:38 +0200
% 64.82/14.32 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 64.82/14.32 % git: non_committed_changes: false
% 64.82/14.32
% 64.82/14.32 % ------ Parsing...
% 64.82/14.32 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 64.82/14.32
% 64.82/14.32 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 1 0s sf_e %
% 64.82/14.32
% 64.82/14.32 % ------ Preprocessing...%
% 64.82/14.32
% 64.82/14.32 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 64.82/14.32 % ------ Proving...
% 64.82/14.32 % ------ Problem Properties
% 64.82/14.32
% 64.82/14.32 %
% 64.82/14.32 % clauses 270
% 64.82/14.32 % conjectures 0
% 64.82/14.32 % EPR 74
% 64.82/14.32 % Horn 195
% 64.82/14.32 % unary 43
% 64.82/14.32 % binary 32
% 64.82/14.32 % lits 1512
% 64.82/14.32 % lits eq 193
% 64.82/14.32 % fd_pure 0
% 64.82/14.32 % fd_pseudo 0
% 64.82/14.32 % fd_cond 0
% 64.82/14.32 % fd_pseudo_cond 50
% 64.82/14.32 % AC symbols 0
% 64.82/14.32
% 64.82/14.32 % ------ Input Options Time Limit: Unbounded
% 64.82/14.32
% 64.82/14.32
% 64.82/14.32 % ------
% 64.82/14.32 % Current options:
% 64.82/14.32 % ------
% 64.82/14.32
% 64.82/14.32
% 64.82/14.32 %
% 64.82/14.32
% 64.82/14.32 % ------ Proving...
% 64.82/14.32 %
% 64.82/14.32
% 64.82/14.32 % SZS status Theorem for theBenchmark.p
% 64.82/14.32
% 64.82/14.32 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 64.82/14.32
% 64.82/14.32
%------------------------------------------------------------------------------