%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO333+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n002.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:58 PM UTC 2026
% Result : Theorem 60.99s 16.46s
% Output : CNFRefutation 60.99s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f37ERROR: Could not build tree for root c_110252ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f14,axiom,
? [X0] :
( rpoint(X0)
& vd1361 = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qe(s1(plural(386)))') ).
fof(f176,plain,
! [X0,X1,X2,X3,X4] :
( ! [X7] :
( ~ rpoint(X7)
| X0 != X7 )
| ! [X6] :
( ~ rpoint(X6)
| X1 != X6 )
| ! [X5] :
( ~ rpoint(X5)
| X2 != X5 )
| ~ rline(X4)
| ~ rR(X1,X0,X2)
| ~ ron(X0,X3)
| ~ ron(X2,X3)
| X3 != X4
| ron(X1,X3) ),
inference(ennf_transformation,[],[f37]) ).
fof(f177,plain,
! [X0,X1,X2,X3,X4] :
( ! [X7] :
( ~ rpoint(X7)
| X0 != X7 )
| ! [X6] :
( ~ rpoint(X6)
| X1 != X6 )
| ! [X5] :
( ~ rpoint(X5)
| X2 != X5 )
| ~ rline(X4)
| ~ rR(X1,X0,X2)
| ~ ron(X0,X3)
| ~ ron(X2,X3)
| X3 != X4
| ron(X1,X3) ),
inference(flattening,[],[f176]) ).
fof(f178,plain,
! [X0,X1,X2] :
( ! [X5] :
( ~ rpoint(X5)
| X0 != X5 )
| ! [X4] :
( ~ rpoint(X4)
| X1 != X4 )
| ! [X3] :
( ~ rpoint(X3)
| X2 != X3 )
| ~ rR(X1,X0,X2)
| ( rR(X1,X2,X0)
& X0 != X1
& X0 != X2
& ~ rR(X0,X1,X2) ) ),
inference(ennf_transformation,[],[f38]) ).
fof(f179,plain,
! [X0,X1,X2] :
( ! [X5] :
( ~ rpoint(X5)
| X0 != X5 )
| ! [X4] :
( ~ rpoint(X4)
| X1 != X4 )
| ! [X3] :
( ~ rpoint(X3)
| X2 != X3 )
| ~ rR(X1,X0,X2)
| ( rR(X1,X2,X0)
& X0 != X1
& X0 != X2
& ~ rR(X0,X1,X2) ) ),
inference(flattening,[],[f178]) ).
fof(f202,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ! [X13] :
( ~ rpoint(X13)
| X0 != X13 )
| ! [X12] :
( ~ rpoint(X12)
| X1 != X12 )
| ! [X11] :
( ~ rpoint(X11)
| X2 != X11 )
| ! [X10] :
( ~ rpoint(X10)
| X3 != X10 )
| ! [X9] :
( ~ rpoint(X9)
| X4 != X9 )
| ! [X8] :
( ~ rline(X8)
| X5 != X8 )
| ! [X7] :
( ~ rline(X7)
| X6 != X7 )
| ~ ron(X0,X5)
| ~ ron(X1,X5)
| ~ ron(X3,X5)
| ~ ron(X2,X6)
| ~ ron(X4,X6)
| X0 = X1
| X0 = X2
| X0 = X3
| X0 = X4
| rR(X0,X1,X3)
| rR(X0,X2,X4)
| vangle(X1,X0,X2) = vangle(X3,X0,X4) ),
inference(ennf_transformation,[],[f52]) ).
fof(f203,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ! [X13] :
( ~ rpoint(X13)
| X0 != X13 )
| ! [X12] :
( ~ rpoint(X12)
| X1 != X12 )
| ! [X11] :
( ~ rpoint(X11)
| X2 != X11 )
| ! [X10] :
( ~ rpoint(X10)
| X3 != X10 )
| ! [X9] :
( ~ rpoint(X9)
| X4 != X9 )
| ! [X8] :
( ~ rline(X8)
| X5 != X8 )
| ! [X7] :
( ~ rline(X7)
| X6 != X7 )
| ~ ron(X0,X5)
| ~ ron(X1,X5)
| ~ ron(X3,X5)
| ~ ron(X2,X6)
| ~ ron(X4,X6)
| X0 = X1
| X0 = X2
| X0 = X3
| X0 = X4
| rR(X0,X1,X3)
| rR(X0,X2,X4)
| vangle(X1,X0,X2) = vangle(X3,X0,X4) ),
inference(flattening,[],[f202]) ).
fof(f208,plain,
! [X0,X1] :
( ! [X3] :
( ~ rpoint(X3)
| X0 != X3 )
| ! [X2] :
( ~ rpoint(X2)
| X1 != X2 )
| X0 = X1
| ? [X4] :
( rline(X4)
& ron(X0,X4)
& ron(X1,X4) ) ),
inference(ennf_transformation,[],[f55]) ).
fof(f209,plain,
! [X0,X1] :
( ! [X3] :
( ~ rpoint(X3)
| X0 != X3 )
| ! [X2] :
( ~ rpoint(X2)
| X1 != X2 )
| X0 = X1
| ? [X4] :
( rline(X4)
& ron(X0,X4)
& ron(X1,X4) ) ),
inference(flattening,[],[f208]) ).
fof(f352,plain,
( rpoint(sK1)
& vd1362 = sK1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X0,sK1)],[f7]) ).
fof(f353,plain,
( rpoint(sK2)
& vd1363 = sK2 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2)],[f13]) ).
fof(f354,plain,
( rpoint(sK3)
& vd1361 = sK3 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X0,sK3)],[f14]) ).
fof(f374,plain,
! [X0,X1] :
( ! [X4] :
( ~ rpoint(X4)
| X0 != X4 )
| ! [X3] :
( ~ rpoint(X3)
| X1 != X3 )
| X0 = X1
| ? [X2] :
( rline(X2)
& ron(X0,X2)
& ron(X1,X2) ) ),
inference(rectify,[],[f209]) ).
fof(f375,plain,
! [X0,X1] :
( ! [X4] :
( ~ rpoint(X4)
| X0 != X4 )
| ! [X3] :
( ~ rpoint(X3)
| X1 != X3 )
| X0 = X1
| ( rline(sK10(X0,X1))
& ron(X0,sK10(X0,X1))
& ron(X1,sK10(X0,X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X2,sK10(X0,X1))],[f374]) ).
fof(f432,plain,
vangle(vd1371,vd1362,vd1363) != vangle(vd1361,vd1363,vd1362),
inference(cnf_transformation,[],[f131]) ).
fof(f435,plain,
rR(vd1371,vd1362,vd1361),
inference(cnf_transformation,[],[f5]) ).
fof(f436,plain,
rpoint(vd1371),
inference(cnf_transformation,[],[f6]) ).
fof(f437,plain,
rpoint(sK1),
inference(cnf_transformation,[],[f352]) ).
fof(f438,plain,
vd1362 = sK1,
inference(cnf_transformation,[],[f352]) ).
fof(f440,plain,
vangle(vd1361,vd1363,vd1362) = vangle(vd1361,vd1362,vd1363),
inference(cnf_transformation,[],[f9]) ).
fof(f441,plain,
vd1362 != vd1363,
inference(cnf_transformation,[],[f10]) ).
fof(f443,plain,
vd1362 != vd1361,
inference(cnf_transformation,[],[f12]) ).
fof(f444,plain,
rpoint(sK2),
inference(cnf_transformation,[],[f353]) ).
fof(f445,plain,
vd1363 = sK2,
inference(cnf_transformation,[],[f353]) ).
fof(f446,plain,
rpoint(sK3),
inference(cnf_transformation,[],[f354]) ).
fof(f447,plain,
vd1361 = sK3,
inference(cnf_transformation,[],[f354]) ).
fof(f486,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rline(X4)
| ~ rR(X1,X0,X2)
| ~ ron(X0,X3)
| ~ ron(X2,X3)
| X3 != X4
| ron(X1,X3) ),
inference(cnf_transformation,[],[f177]) ).
fof(f490,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X1,X0,X2)
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[],[f179]) ).
fof(f507,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ rpoint(X13)
| X0 != X13
| ~ rpoint(X12)
| X1 != X12
| ~ rpoint(X11)
| X2 != X11
| ~ rpoint(X10)
| X3 != X10
| ~ rpoint(X9)
| X4 != X9
| ~ rline(X8)
| X5 != X8
| ~ rline(X7)
| X6 != X7
| ~ ron(X0,X5)
| ~ ron(X1,X5)
| ~ ron(X3,X5)
| ~ ron(X2,X6)
| ~ ron(X4,X6)
| X0 = X1
| X0 = X2
| X0 = X3
| X0 = X4
| rR(X0,X1,X3)
| rR(X0,X2,X4)
| vangle(X1,X0,X2) = vangle(X3,X0,X4) ),
inference(cnf_transformation,[],[f203]) ).
fof(f512,plain,
! [X3,X0,X1,X4] :
( ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X1 != X3
| X0 = X1
| rline(sK10(X0,X1)) ),
inference(cnf_transformation,[],[f375]) ).
fof(f513,plain,
! [X3,X0,X1,X4] :
( ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X1 != X3
| X0 = X1
| ron(X0,sK10(X0,X1)) ),
inference(cnf_transformation,[],[f375]) ).
fof(f514,plain,
! [X3,X0,X1,X4] :
( ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X1 != X3
| X0 = X1
| ron(X1,sK10(X0,X1)) ),
inference(cnf_transformation,[],[f375]) ).
fof(f696,plain,
vangle(vd1371,sK1,sK2) != vangle(sK3,sK2,sK1),
inference(definition_unfolding,[],[f432,f438,f445,f447,f445,f438]) ).
fof(f699,plain,
rR(vd1371,sK1,sK3),
inference(definition_unfolding,[],[f435,f438,f447]) ).
fof(f700,plain,
vangle(sK3,sK2,sK1) = vangle(sK3,sK1,sK2),
inference(definition_unfolding,[],[f440,f447,f445,f438,f447,f438,f445]) ).
fof(f701,plain,
sK1 != sK2,
inference(definition_unfolding,[],[f441,f438,f445]) ).
fof(f703,plain,
sK1 != sK3,
inference(definition_unfolding,[],[f443,f438,f447]) ).
fof(f872,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rline(X4)
| ~ rR(X1,X0,X2)
| ~ ron(X0,X4)
| ~ ron(X2,X4)
| ron(X1,X4) ),
inference(equality_resolution,[],[f486]) ).
fof(f873,plain,
! [X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| ~ rline(X4)
| ~ rR(X1,X0,X5)
| ~ ron(X0,X4)
| ~ ron(X5,X4)
| ron(X1,X4) ),
inference(equality_resolution,[],[f872]) ).
fof(f874,plain,
! [X0,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| ~ rpoint(X5)
| ~ rline(X4)
| ~ rR(X6,X0,X5)
| ~ ron(X0,X4)
| ~ ron(X5,X4)
| ron(X6,X4) ),
inference(equality_resolution,[],[f873]) ).
fof(f875,plain,
! [X6,X7,X4,X5] :
( ~ rpoint(X7)
| ~ rpoint(X6)
| ~ rpoint(X5)
| ~ rline(X4)
| ~ rR(X6,X7,X5)
| ~ ron(X7,X4)
| ~ ron(X5,X4)
| ron(X6,X4) ),
inference(equality_resolution,[],[f874]) ).
fof(f876,plain,
! [X3,X0,X1,X4,X5] :
( ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| ~ rR(X1,X0,X3)
| ~ rR(X0,X1,X3) ),
inference(equality_resolution,[],[f490]) ).
fof(f877,plain,
! [X3,X0,X4,X5] :
( ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rR(X4,X0,X3)
| ~ rR(X0,X4,X3) ),
inference(equality_resolution,[],[f876]) ).
fof(f878,plain,
! [X3,X4,X5] :
( ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rR(X4,X5,X3)
| ~ rR(X5,X4,X3) ),
inference(equality_resolution,[],[f877]) ).
fof(f932,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X5,X12,X13] :
( ~ rpoint(X13)
| X0 != X13
| ~ rpoint(X12)
| X1 != X12
| ~ rpoint(X11)
| X2 != X11
| ~ rpoint(X10)
| X3 != X10
| ~ rpoint(X9)
| X4 != X9
| ~ rline(X8)
| X5 != X8
| ~ rline(X7)
| ~ ron(X0,X5)
| ~ ron(X1,X5)
| ~ ron(X3,X5)
| ~ ron(X2,X7)
| ~ ron(X4,X7)
| X0 = X1
| X0 = X2
| X0 = X3
| X0 = X4
| rR(X0,X1,X3)
| rR(X0,X2,X4)
| vangle(X1,X0,X2) = vangle(X3,X0,X4) ),
inference(equality_resolution,[],[f507]) ).
fof(f933,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X12,X13] :
( ~ rpoint(X13)
| X0 != X13
| ~ rpoint(X12)
| X1 != X12
| ~ rpoint(X11)
| X2 != X11
| ~ rpoint(X10)
| X3 != X10
| ~ rpoint(X9)
| X4 != X9
| ~ rline(X8)
| ~ rline(X7)
| ~ ron(X0,X8)
| ~ ron(X1,X8)
| ~ ron(X3,X8)
| ~ ron(X2,X7)
| ~ ron(X4,X7)
| X0 = X1
| X0 = X2
| X0 = X3
| X0 = X4
| rR(X0,X1,X3)
| rR(X0,X2,X4)
| vangle(X1,X0,X2) = vangle(X3,X0,X4) ),
inference(equality_resolution,[],[f932]) ).
fof(f934,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X12,X13] :
( ~ rpoint(X13)
| X0 != X13
| ~ rpoint(X12)
| X1 != X12
| ~ rpoint(X11)
| X2 != X11
| ~ rpoint(X10)
| X3 != X10
| ~ rpoint(X9)
| ~ rline(X8)
| ~ rline(X7)
| ~ ron(X0,X8)
| ~ ron(X1,X8)
| ~ ron(X3,X8)
| ~ ron(X2,X7)
| ~ ron(X9,X7)
| X0 = X1
| X0 = X2
| X0 = X3
| X0 = X9
| rR(X0,X1,X3)
| rR(X0,X2,X9)
| vangle(X1,X0,X2) = vangle(X3,X0,X9) ),
inference(equality_resolution,[],[f933]) ).
fof(f935,plain,
! [X2,X10,X0,X11,X1,X8,X9,X7,X12,X13] :
( ~ rpoint(X13)
| X0 != X13
| ~ rpoint(X12)
| X1 != X12
| ~ rpoint(X11)
| X2 != X11
| ~ rpoint(X10)
| ~ rpoint(X9)
| ~ rline(X8)
| ~ rline(X7)
| ~ ron(X0,X8)
| ~ ron(X1,X8)
| ~ ron(X10,X8)
| ~ ron(X2,X7)
| ~ ron(X9,X7)
| X0 = X1
| X0 = X2
| X0 = X10
| X0 = X9
| rR(X0,X1,X10)
| rR(X0,X2,X9)
| vangle(X1,X0,X2) = vangle(X10,X0,X9) ),
inference(equality_resolution,[],[f934]) ).
fof(f936,plain,
! [X10,X0,X11,X1,X8,X9,X7,X12,X13] :
( ~ rpoint(X13)
| X0 != X13
| ~ rpoint(X12)
| X1 != X12
| ~ rpoint(X11)
| ~ rpoint(X10)
| ~ rpoint(X9)
| ~ rline(X8)
| ~ rline(X7)
| ~ ron(X0,X8)
| ~ ron(X1,X8)
| ~ ron(X10,X8)
| ~ ron(X11,X7)
| ~ ron(X9,X7)
| X0 = X1
| X0 = X11
| X0 = X10
| X0 = X9
| rR(X0,X1,X10)
| rR(X0,X11,X9)
| vangle(X10,X0,X9) = vangle(X1,X0,X11) ),
inference(equality_resolution,[],[f935]) ).
fof(f937,plain,
! [X10,X0,X11,X8,X9,X7,X12,X13] :
( ~ rpoint(X13)
| X0 != X13
| ~ rpoint(X12)
| ~ rpoint(X11)
| ~ rpoint(X10)
| ~ rpoint(X9)
| ~ rline(X8)
| ~ rline(X7)
| ~ ron(X0,X8)
| ~ ron(X12,X8)
| ~ ron(X10,X8)
| ~ ron(X11,X7)
| ~ ron(X9,X7)
| X0 = X12
| X0 = X11
| X0 = X10
| X0 = X9
| rR(X0,X12,X10)
| rR(X0,X11,X9)
| vangle(X10,X0,X9) = vangle(X12,X0,X11) ),
inference(equality_resolution,[],[f936]) ).
fof(f938,plain,
! [X10,X11,X8,X9,X7,X12,X13] :
( ~ rpoint(X13)
| ~ rpoint(X12)
| ~ rpoint(X11)
| ~ rpoint(X10)
| ~ rpoint(X9)
| ~ rline(X8)
| ~ rline(X7)
| ~ ron(X13,X8)
| ~ ron(X12,X8)
| ~ ron(X10,X8)
| ~ ron(X11,X7)
| ~ ron(X9,X7)
| X12 = X13
| X11 = X13
| X10 = X13
| X9 = X13
| rR(X13,X12,X10)
| rR(X13,X11,X9)
| vangle(X10,X13,X9) = vangle(X12,X13,X11) ),
inference(equality_resolution,[],[f937]) ).
fof(f948,plain,
! [X3,X0,X4] :
( ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X0 = X3
| ron(X3,sK10(X0,X3)) ),
inference(equality_resolution,[],[f514]) ).
fof(f949,plain,
! [X3,X4] :
( ~ rpoint(X4)
| ~ rpoint(X3)
| X3 = X4
| ron(X3,sK10(X4,X3)) ),
inference(equality_resolution,[],[f948]) ).
fof(f950,plain,
! [X3,X0,X4] :
( ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X0 = X3
| ron(X0,sK10(X0,X3)) ),
inference(equality_resolution,[],[f513]) ).
fof(f951,plain,
! [X3,X4] :
( ~ rpoint(X4)
| ~ rpoint(X3)
| X3 = X4
| ron(X4,sK10(X4,X3)) ),
inference(equality_resolution,[],[f950]) ).
fof(f952,plain,
! [X3,X0,X4] :
( ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X0 = X3
| rline(sK10(X0,X3)) ),
inference(equality_resolution,[],[f512]) ).
fof(f953,plain,
! [X3,X4] :
( ~ rpoint(X4)
| ~ rpoint(X3)
| X3 = X4
| rline(sK10(X4,X3)) ),
inference(equality_resolution,[],[f952]) ).
tcf(c_49,negated_conjecture,
vangle(vd1371,sK1,sK2) != vangle(sK3,sK2,sK1),
inference(cnf_transformation,[],[f696]) ).
tcf(c_52,plain,
rR(vd1371,sK1,sK3),
inference(cnf_transformation,[],[f699]) ).
tcf(c_53,plain,
rpoint(vd1371),
inference(cnf_transformation,[],[f436]) ).
tcf(c_54,plain,
rpoint(sK1),
inference(cnf_transformation,[],[f437]) ).
tcf(c_56,plain,
vangle(sK3,sK1,sK2) = vangle(sK3,sK2,sK1),
inference(cnf_transformation,[],[f700]) ).
tcf(c_57,plain,
sK1 != sK2,
inference(cnf_transformation,[],[f701]) ).
tcf(c_59,plain,
sK1 != sK3,
inference(cnf_transformation,[],[f703]) ).
tcf(c_60,plain,
rpoint(sK2),
inference(cnf_transformation,[],[f444]) ).
tcf(c_61,plain,
rpoint(sK3),
inference(cnf_transformation,[],[f446]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ron(X0,X3)
| ~ rline(X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[],[f875]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(X1,X0,X2)
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[],[f878]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(X0,X1,X1) ),
inference(cnf_transformation,[],[f1496]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( rR(X6,X5,X0)
| rR(X6,X2,X4)
| ( X5 = X6 )
| ( X4 = X6 )
| ( X2 = X6 )
| ( X0 = X6 )
| ( vangle(X2,X6,X5) = vangle(X4,X6,X0) )
| ~ rline(X3)
| ~ rline(X1)
| ~ rpoint(X6)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ ron(X6,X3)
| ~ ron(X5,X1)
| ~ ron(X4,X3)
| ~ ron(X2,X3)
| ~ ron(X0,X1) ),
inference(cnf_transformation,[],[f938]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i] :
( ron(X0,sK10(X1,X0))
| ( X0 = X1 )
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(cnf_transformation,[],[f949]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i] :
( ron(X1,sK10(X1,X0))
| ( X0 = X1 )
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(cnf_transformation,[],[f951]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i] :
( rline(sK10(X1,X0))
| ( X0 = X1 )
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(cnf_transformation,[],[f953]) ).
tcf(c_3910,plain,
vangle(vd1371,sK1,sK2) != vangle(sK3,sK1,sK2),
inference(light_normalisation,[status(thm)],[c_49,c_56]) ).
tcf(c_16487,plain,
vangle(vd1371,sK1,sK2) != vangle(sK3,sK1,sK2),
inference(subtyping,[status(esa)],[c_3910]) ).
tcf(c_16665,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rpoint_1: iProver_rpoint_1] :
( rline(sK10(X0_iProver_rpoint_1,X1_iProver_rpoint_1))
| ( X1_iProver_rpoint_1 = X0_iProver_rpoint_1 )
| ~ rpoint(X1_iProver_rpoint_1)
| ~ rpoint(X0_iProver_rpoint_1) ),
inference(subtyping,[status(esa)],[c_127]) ).
tcf(c_16666,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rpoint_1: iProver_rpoint_1] :
( ron(X0_iProver_rpoint_1,sK10(X0_iProver_rpoint_1,X1_iProver_rpoint_1))
| ( X1_iProver_rpoint_1 = X0_iProver_rpoint_1 )
| ~ rpoint(X1_iProver_rpoint_1)
| ~ rpoint(X0_iProver_rpoint_1) ),
inference(subtyping,[status(esa)],[c_126]) ).
tcf(c_16667,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rpoint_1: iProver_rpoint_1] :
( ron(X0_iProver_rpoint_1,sK10(X1_iProver_rpoint_1,X0_iProver_rpoint_1))
| ( X0_iProver_rpoint_1 = X1_iProver_rpoint_1 )
| ~ rpoint(X1_iProver_rpoint_1)
| ~ rpoint(X0_iProver_rpoint_1) ),
inference(subtyping,[status(esa)],[c_125]) ).
tcf(c_16672,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X0_iProver_rline_1: iProver_rline_1,X1_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rline_1: iProver_rline_1,X2_iProver_rpoint_1: iProver_rpoint_1,X3_iProver_rpoint_1: iProver_rpoint_1,X4_iProver_rpoint_1: iProver_rpoint_1] :
( rR(X0_iProver_rpoint_1,X3_iProver_rpoint_1,X4_iProver_rpoint_1)
| rR(X0_iProver_rpoint_1,X1_iProver_rpoint_1,X2_iProver_rpoint_1)
| ( X4_iProver_rpoint_1 = X0_iProver_rpoint_1 )
| ( X3_iProver_rpoint_1 = X0_iProver_rpoint_1 )
| ( X2_iProver_rpoint_1 = X0_iProver_rpoint_1 )
| ( X1_iProver_rpoint_1 = X0_iProver_rpoint_1 )
| ( vangle(X1_iProver_rpoint_1,X0_iProver_rpoint_1,X3_iProver_rpoint_1) = vangle(X2_iProver_rpoint_1,X0_iProver_rpoint_1,X4_iProver_rpoint_1) )
| ~ rline(X1_iProver_rline_1)
| ~ rline(X0_iProver_rline_1)
| ~ rpoint(X4_iProver_rpoint_1)
| ~ rpoint(X3_iProver_rpoint_1)
| ~ rpoint(X2_iProver_rpoint_1)
| ~ rpoint(X1_iProver_rpoint_1)
| ~ rpoint(X0_iProver_rpoint_1)
| ~ ron(X4_iProver_rpoint_1,X1_iProver_rline_1)
| ~ ron(X3_iProver_rpoint_1,X1_iProver_rline_1)
| ~ ron(X2_iProver_rpoint_1,X0_iProver_rline_1)
| ~ ron(X1_iProver_rpoint_1,X0_iProver_rline_1)
| ~ ron(X0_iProver_rpoint_1,X0_iProver_rline_1) ),
inference(subtyping,[status(esa)],[c_120]) ).
tcf(c_16690,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rpoint_1: iProver_rpoint_1] :
( ~ rpoint(X1_iProver_rpoint_1)
| ~ rpoint(X0_iProver_rpoint_1)
| ~ rR(X0_iProver_rpoint_1,X1_iProver_rpoint_1,X1_iProver_rpoint_1) ),
inference(subtyping,[status(esa)],[c_102]) ).
tcf(c_16691,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rpoint_1: iProver_rpoint_1,X2_iProver_rpoint_1: iProver_rpoint_1] :
( ~ rpoint(X2_iProver_rpoint_1)
| ~ rpoint(X1_iProver_rpoint_1)
| ~ rpoint(X0_iProver_rpoint_1)
| ~ rR(X1_iProver_rpoint_1,X0_iProver_rpoint_1,X2_iProver_rpoint_1)
| ~ rR(X0_iProver_rpoint_1,X1_iProver_rpoint_1,X2_iProver_rpoint_1) ),
inference(subtyping,[status(esa)],[c_101]) ).
tcf(c_16692,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X0_iProver_rline_1: iProver_rline_1,X1_iProver_rpoint_1: iProver_rpoint_1,X2_iProver_rpoint_1: iProver_rpoint_1] :
( ron(X0_iProver_rpoint_1,X0_iProver_rline_1)
| ~ rline(X0_iProver_rline_1)
| ~ rpoint(X2_iProver_rpoint_1)
| ~ rpoint(X1_iProver_rpoint_1)
| ~ rpoint(X0_iProver_rpoint_1)
| ~ ron(X2_iProver_rpoint_1,X0_iProver_rline_1)
| ~ ron(X1_iProver_rpoint_1,X0_iProver_rline_1)
| ~ rR(X0_iProver_rpoint_1,X1_iProver_rpoint_1,X2_iProver_rpoint_1) ),
inference(subtyping,[status(esa)],[c_100]) ).
tcf(c_16733,plain,
sK1 != sK3,
inference(subtyping,[status(esa)],[c_59]) ).
tcf(c_16735,plain,
sK1 != sK2,
inference(subtyping,[status(esa)],[c_57]) ).
tcf(c_16762,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1] : X0_iProver_rpoint_1 = X0_iProver_rpoint_1,
theory(equality) ).
tcf(c_16765,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rpoint_1: iProver_rpoint_1,X2_iProver_rpoint_1: iProver_rpoint_1] :
( ( X2_iProver_rpoint_1 = X0_iProver_rpoint_1 )
| ( X2_iProver_rpoint_1 != X1_iProver_rpoint_1 )
| ( X0_iProver_rpoint_1 != X1_iProver_rpoint_1 ) ),
theory(equality) ).
tcf(c_16769,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rpoint_1: iProver_rpoint_1,X2_iProver_rpoint_1: iProver_rpoint_1,X3_iProver_rpoint_1: iProver_rpoint_1,X4_iProver_rpoint_1: iProver_rpoint_1,X5_iProver_rpoint_1: iProver_rpoint_1] :
( rR(X0_iProver_rpoint_1,X2_iProver_rpoint_1,X4_iProver_rpoint_1)
| ~ rR(X1_iProver_rpoint_1,X3_iProver_rpoint_1,X5_iProver_rpoint_1)
| ( X4_iProver_rpoint_1 != X5_iProver_rpoint_1 )
| ( X2_iProver_rpoint_1 != X3_iProver_rpoint_1 )
| ( X0_iProver_rpoint_1 != X1_iProver_rpoint_1 ) ),
theory(equality) ).
tcf(c_16786,plain,
sK3 = sK3,
inference(instantiation,[status(thm)],[c_16762]) ).
tcf(c_23850,plain,
( rline(sK10(sK3,sK1))
| ( sK1 = sK3 )
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(instantiation,[status(thm)],[c_16665]) ).
tcf(c_23852,plain,
( rline(sK10(sK2,sK1))
| ( sK1 = sK2 )
| ~ rpoint(sK2)
| ~ rpoint(sK1) ),
inference(instantiation,[status(thm)],[c_16665]) ).
tcf(c_23876,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1] :
( ( sK1 = sK3 )
| ( sK3 != X0_iProver_rpoint_1 )
| ( sK1 != X0_iProver_rpoint_1 ) ),
inference(instantiation,[status(thm)],[c_16765]) ).
tcf(c_23878,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1] :
( ( sK1 = sK2 )
| ( sK2 != X0_iProver_rpoint_1 )
| ( sK1 != X0_iProver_rpoint_1 ) ),
inference(instantiation,[status(thm)],[c_16765]) ).
tcf(c_23903,plain,
( ron(sK3,sK10(sK3,sK1))
| ( sK1 = sK3 )
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(instantiation,[status(thm)],[c_16666]) ).
tcf(c_23905,plain,
( ron(sK2,sK10(sK2,sK1))
| ( sK1 = sK2 )
| ~ rpoint(sK2)
| ~ rpoint(sK1) ),
inference(instantiation,[status(thm)],[c_16666]) ).
tcf(c_23915,plain,
( ron(sK1,sK10(sK3,sK1))
| ( sK1 = sK3 )
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(instantiation,[status(thm)],[c_16667]) ).
tcf(c_24025,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rpoint_1: iProver_rpoint_1,X2_iProver_rpoint_1: iProver_rpoint_1] :
( rR(X0_iProver_rpoint_1,X1_iProver_rpoint_1,X2_iProver_rpoint_1)
| ~ rR(vd1371,sK1,sK3)
| ( X2_iProver_rpoint_1 != sK3 )
| ( X1_iProver_rpoint_1 != sK1 )
| ( X0_iProver_rpoint_1 != vd1371 ) ),
inference(instantiation,[status(thm)],[c_16769]) ).
tcf(c_24247,plain,
( ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ rR(sK1,vd1371,sK3)
| ~ rR(vd1371,sK1,sK3) ),
inference(instantiation,[status(thm)],[c_16691]) ).
tcf(c_26570,plain,
( ( sK1 = sK3 )
| ( sK3 != sK1 )
| ( sK1 != sK1 ) ),
inference(instantiation,[status(thm)],[c_23876]) ).
tcf(c_26571,plain,
sK1 = sK1,
inference(instantiation,[status(thm)],[c_16762]) ).
tcf(c_26844,plain,
( ( sK1 = sK2 )
| ( sK2 != sK1 )
| ( sK1 != sK1 ) ),
inference(instantiation,[status(thm)],[c_23878]) ).
tcf(c_27858,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rpoint_1: iProver_rpoint_1] :
( rR(vd1371,X0_iProver_rpoint_1,X1_iProver_rpoint_1)
| ~ rR(vd1371,sK1,sK3)
| ( vd1371 != vd1371 )
| ( X1_iProver_rpoint_1 != sK3 )
| ( X0_iProver_rpoint_1 != sK1 ) ),
inference(instantiation,[status(thm)],[c_24025]) ).
tcf(c_27859,plain,
vd1371 = vd1371,
inference(instantiation,[status(thm)],[c_16762]) ).
tcf(c_35934,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1] :
( rR(vd1371,vd1371,X0_iProver_rpoint_1)
| ~ rR(vd1371,sK1,sK3)
| ( vd1371 != sK1 )
| ( vd1371 != vd1371 )
| ( X0_iProver_rpoint_1 != sK3 ) ),
inference(instantiation,[status(thm)],[c_27858]) ).
tcf(c_35935,plain,
( rR(vd1371,vd1371,sK3)
| ~ rR(vd1371,sK1,sK3)
| ( sK3 != sK3 )
| ( vd1371 != sK1 )
| ( vd1371 != vd1371 ) ),
inference(instantiation,[status(thm)],[c_35934]) ).
tcf(c_46186,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1] :
( ~ rpoint(vd1371)
| ~ rpoint(X0_iProver_rpoint_1)
| ~ rR(vd1371,vd1371,X0_iProver_rpoint_1) ),
inference(instantiation,[status(thm)],[c_16691]) ).
tcf(c_46187,plain,
( ~ rpoint(sK3)
| ~ rpoint(vd1371)
| ~ rR(vd1371,vd1371,sK3) ),
inference(instantiation,[status(thm)],[c_46186]) ).
tcf(c_99052,plain,
! [X0_iProver_rline_1: iProver_rline_1,X1_iProver_rline_1: iProver_rline_1] :
( rR(sK1,sK2,sK2)
| rR(sK1,vd1371,sK3)
| ( sK3 = sK1 )
| ( sK2 = sK1 )
| ( vd1371 = sK1 )
| ( vangle(vd1371,sK1,sK2) = vangle(sK3,sK1,sK2) )
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ rline(X1_iProver_rline_1)
| ~ rline(X0_iProver_rline_1)
| ~ ron(sK3,X0_iProver_rline_1)
| ~ ron(sK2,X1_iProver_rline_1)
| ~ ron(sK1,X0_iProver_rline_1)
| ~ ron(vd1371,X0_iProver_rline_1) ),
inference(instantiation,[status(thm)],[c_16672]) ).
tcf(c_99199,plain,
( ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rR(sK1,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_16690]) ).
tcf(c_100958,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X0_iProver_rline_1: iProver_rline_1,X1_iProver_rpoint_1: iProver_rpoint_1] :
( ron(vd1371,X0_iProver_rline_1)
| ~ rpoint(vd1371)
| ~ rline(X0_iProver_rline_1)
| ~ rpoint(X1_iProver_rpoint_1)
| ~ rpoint(X0_iProver_rpoint_1)
| ~ ron(X1_iProver_rpoint_1,X0_iProver_rline_1)
| ~ ron(X0_iProver_rpoint_1,X0_iProver_rline_1)
| ~ rR(vd1371,X0_iProver_rpoint_1,X1_iProver_rpoint_1) ),
inference(instantiation,[status(thm)],[c_16692]) ).
tcf(c_103344,plain,
! [X0_iProver_rline_1: iProver_rline_1] :
( ron(vd1371,X0_iProver_rline_1)
| ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ rline(X0_iProver_rline_1)
| ~ ron(sK3,X0_iProver_rline_1)
| ~ ron(sK1,X0_iProver_rline_1)
| ~ rR(vd1371,sK1,sK3) ),
inference(instantiation,[status(thm)],[c_100958]) ).
tcf(c_105523,plain,
! [X0_iProver_rline_1: iProver_rline_1] :
( rR(sK1,sK2,sK2)
| rR(sK1,vd1371,sK3)
| ( sK3 = sK1 )
| ( sK2 = sK1 )
| ( vd1371 = sK1 )
| ( vangle(vd1371,sK1,sK2) = vangle(sK3,sK1,sK2) )
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ rline(X0_iProver_rline_1)
| ~ ron(sK3,X0_iProver_rline_1)
| ~ ron(sK1,X0_iProver_rline_1)
| ~ ron(vd1371,X0_iProver_rline_1)
| ~ rline(sK10(sK2,sK1))
| ~ ron(sK2,sK10(sK2,sK1)) ),
inference(instantiation,[status(thm)],[c_99052]) ).
tcf(c_108204,plain,
( rR(sK1,sK2,sK2)
| rR(sK1,vd1371,sK3)
| ( sK3 = sK1 )
| ( sK2 = sK1 )
| ( vd1371 = sK1 )
| ( vangle(vd1371,sK1,sK2) = vangle(sK3,sK1,sK2) )
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ rline(sK10(sK3,sK1))
| ~ rline(sK10(sK2,sK1))
| ~ ron(sK3,sK10(sK3,sK1))
| ~ ron(sK2,sK10(sK2,sK1))
| ~ ron(sK1,sK10(sK3,sK1))
| ~ ron(vd1371,sK10(sK3,sK1)) ),
inference(instantiation,[status(thm)],[c_105523]) ).
tcf(c_110221,plain,
( ron(vd1371,sK10(sK3,sK1))
| ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ rline(sK10(sK3,sK1))
| ~ rR(vd1371,sK1,sK3)
| ~ ron(sK3,sK10(sK3,sK1))
| ~ ron(sK1,sK10(sK3,sK1)) ),
inference(instantiation,[status(thm)],[c_103344]) ).
tcf(c_110252,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_110221,c_108204,c_99199,c_46187,c_35935,c_27859,c_26844,c_26571,c_26570,c_24247,c_23915,c_23905,c_23903,c_23852,c_23850,c_16735,c_16733,c_16487,c_16786,c_52,c_53,c_54,c_60,c_61]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO333+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n002.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 11:59:48 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 60.99/16.46 % SZS status Started for theBenchmark.p
% 60.99/16.46 % SZS status Theorem for theBenchmark.p
% 60.99/16.46
% 60.99/16.46 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 60.99/16.46
% 60.99/16.46 % ------ iProver source info
% 60.99/16.46
% 60.99/16.46 % git: date: 2026-07-19 20:42:38 +0200
% 60.99/16.46 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 60.99/16.46 % git: non_committed_changes: false
% 60.99/16.46
% 60.99/16.46 % ------ Parsing...
% 60.99/16.46 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 60.99/16.46
% 60.99/16.46 % ------ Preprocessing... sup_sim: 1 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 60.99/16.46
% 60.99/16.46 % ------ Preprocessing... gs_s sp: 14 0s gs_e snvd_s sp: 0 0s snvd_e %
% 60.99/16.46
% 60.99/16.46 % ------ Preprocessing... sf_s rm: 8 0s sf_e sf_s rm: 0 0s sf_e
% 60.99/16.46 % ------ Proving...
% 60.99/16.46 % ------ Problem Properties
% 60.99/16.46
% 60.99/16.46 %
% 60.99/16.46 % clauses 266
% 60.99/16.46 % conjectures 0
% 60.99/16.46 % EPR 61
% 60.99/16.46 % Horn 171
% 60.99/16.46 % unary 16
% 60.99/16.46 % binary 42
% 60.99/16.46 % lits 1687
% 60.99/16.46 % lits eq 279
% 60.99/16.46 % fd_pure 0
% 60.99/16.46 % fd_pseudo 0
% 60.99/16.46 % fd_cond 0
% 60.99/16.46 % fd_pseudo_cond 64
% 60.99/16.46 % AC symbols 0
% 60.99/16.46
% 60.99/16.46 % ------ Input Options Time Limit: Unbounded
% 60.99/16.46
% 60.99/16.46
% 60.99/16.46 % ------
% 60.99/16.46 % Current options:
% 60.99/16.46 % ------
% 60.99/16.46
% 60.99/16.46
% 60.99/16.46 %
% 60.99/16.46
% 60.99/16.46 % ------ Proving...
% 60.99/16.46 %
% 60.99/16.46
% 60.99/16.46 % SZS status Theorem for theBenchmark.p
% 60.99/16.46
% 60.99/16.46 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 60.99/16.46
% 60.99/16.46
%------------------------------------------------------------------------------