%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO337+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 : n010.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:59 PM UTC 2026
% Result : Theorem 130.09s 31.47s
% Output : CNFRefutation 130.09s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f33ERROR: Could not build tree for root c_437366ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
vf(vd1378,vd1363) = vf(vd1361,vd1362),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct1(397), 1381, 0)') ).
fof(f4,axiom,
vf(vd1363,vd1378) = vf(vd1361,vd1362),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct2(396), 1380, 0)') ).
fof(f5,axiom,
rR(vd1378,vd1361,vd1363),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct1(396), 1379, 0)') ).
fof(f6,axiom,
rpoint(vd1378),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(396, 0)') ).
fof(f7,axiom,
? [X0] :
( rpoint(X0)
& vd1363 = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qe(s3(plural(386)))') ).
fof(f14,axiom,
? [X0] :
( rpoint(X0)
& vd1361 = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qe(s1(plural(386)))') ).
fof(f145,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,[],[f57]) ).
fof(f146,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,[],[f145]) ).
fof(f153,plain,
! [X0,X1,X2] :
( ! [X5] :
( ~ rpoint(X5)
| X0 != X5 )
| ! [X4] :
( ~ rpoint(X4)
| X1 != X4 )
| ! [X3] :
( ~ rpoint(X3)
| X2 != X3 )
| X0 = X1
| X0 = X2
| X1 = X2
| vf(X0,X1) != vf(X0,X2)
| ! [X6,X7,X8,X9] :
( ~ rpoint(X7)
| ~ rR(X1,X0,X6)
| ~ rpoint(X9)
| ~ rR(X2,X0,X8)
| X8 != X9
| X6 != X7
| vangle(X0,X1,X2) = vangle(X0,X2,X1) ) ),
inference(ennf_transformation,[],[f23]) ).
fof(f154,plain,
! [X0,X1,X2] :
( ! [X5] :
( ~ rpoint(X5)
| X0 != X5 )
| ! [X4] :
( ~ rpoint(X4)
| X1 != X4 )
| ! [X3] :
( ~ rpoint(X3)
| X2 != X3 )
| X0 = X1
| X0 = X2
| X1 = X2
| vf(X0,X1) != vf(X0,X2)
| ! [X6,X7,X8,X9] :
( ~ rpoint(X7)
| ~ rR(X1,X0,X6)
| ~ rpoint(X9)
| ~ rR(X2,X0,X8)
| X8 != X9
| X6 != X7
| vangle(X0,X1,X2) = vangle(X0,X2,X1) ) ),
inference(flattening,[],[f153]) ).
fof(f167,plain,
! [X0,X1,X2,X3] :
( ! [X7] :
( ~ rpoint(X7)
| X0 != X7 )
| ! [X6] :
( ~ rpoint(X6)
| X1 != X6 )
| ! [X5] :
( ~ rpoint(X5)
| X2 != X5 )
| ! [X4] :
( ~ rpoint(X4)
| X3 != X4 )
| ~ rR(X1,X0,X2)
| ~ rR(X3,X0,X1)
| rR(X3,X0,X2) ),
inference(ennf_transformation,[],[f84]) ).
fof(f168,plain,
! [X0,X1,X2,X3] :
( ! [X7] :
( ~ rpoint(X7)
| X0 != X7 )
| ! [X6] :
( ~ rpoint(X6)
| X1 != X6 )
| ! [X5] :
( ~ rpoint(X5)
| X2 != X5 )
| ! [X4] :
( ~ rpoint(X4)
| X3 != X4 )
| ~ rR(X1,X0,X2)
| ~ rR(X3,X0,X1)
| rR(X3,X0,X2) ),
inference(flattening,[],[f167]) ).
fof(f169,plain,
! [X0,X1,X2,X3] :
( ! [X7] :
( ~ rpoint(X7)
| X0 != X7 )
| ! [X6] :
( ~ rpoint(X6)
| X1 != X6 )
| ! [X5] :
( ~ rpoint(X5)
| X2 != X5 )
| ! [X4] :
( ~ rpoint(X4)
| X3 != X4 )
| ~ rR(X1,X0,X2)
| ~ rR(X1,X0,X3)
| ~ rR(X1,X2,X3) ),
inference(ennf_transformation,[],[f83]) ).
fof(f170,plain,
! [X0,X1,X2,X3] :
( ! [X7] :
( ~ rpoint(X7)
| X0 != X7 )
| ! [X6] :
( ~ rpoint(X6)
| X1 != X6 )
| ! [X5] :
( ~ rpoint(X5)
| X2 != X5 )
| ! [X4] :
( ~ rpoint(X4)
| X3 != X4 )
| ~ rR(X1,X0,X2)
| ~ rR(X1,X0,X3)
| ~ rR(X1,X2,X3) ),
inference(flattening,[],[f169]) ).
fof(f183,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,[],[f33]) ).
fof(f184,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,[],[f183]) ).
fof(f185,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,[],[f32]) ).
fof(f186,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,[],[f185]) ).
fof(f187,plain,
! [X0,X1,X2,X3] :
( ! [X7] :
( ~ rpoint(X7)
| X0 != X7 )
| ! [X6] :
( ~ rpoint(X6)
| X1 != X6 )
| ! [X5] :
( ~ rpoint(X5)
| X2 != X5 )
| ! [X4] :
( ~ rpoint(X4)
| X3 != X4 )
| ~ rR(X1,X0,X2)
| ~ rR(X2,X1,X3)
| rR(X1,X0,X3) ),
inference(ennf_transformation,[],[f31]) ).
fof(f188,plain,
! [X0,X1,X2,X3] :
( ! [X7] :
( ~ rpoint(X7)
| X0 != X7 )
| ! [X6] :
( ~ rpoint(X6)
| X1 != X6 )
| ! [X5] :
( ~ rpoint(X5)
| X2 != X5 )
| ! [X4] :
( ~ rpoint(X4)
| X3 != X4 )
| ~ rR(X1,X0,X2)
| ~ rR(X2,X1,X3)
| rR(X1,X0,X3) ),
inference(flattening,[],[f187]) ).
fof(f205,plain,
! [X0,X1,X2,X3] :
( ~ rline(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ ron(X2,X0)
| ? [X4] :
( rpoint(X4)
& ron(X4,X0)
& X4 != X2 ) ),
inference(ennf_transformation,[],[f110]) ).
fof(f206,plain,
! [X0,X1,X2,X3] :
( ~ rline(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ ron(X2,X0)
| ? [X4] :
( rpoint(X4)
& ron(X4,X0)
& X4 != X2 ) ),
inference(flattening,[],[f205]) ).
fof(f211,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,[],[f60]) ).
fof(f212,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,[],[f211]) ).
fof(f336,plain,
( rpoint(sK5)
& vd1363 = sK5 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X0,sK5)],[f7]) ).
fof(f337,plain,
( rpoint(sK6)
& vd1362 = sK6 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X0,sK6)],[f13]) ).
fof(f345,plain,
! [X0,X1,X2] :
( ! [X9] :
( ~ rpoint(X9)
| X0 != X9 )
| ! [X8] :
( ~ rpoint(X8)
| X1 != X8 )
| ! [X7] :
( ~ rpoint(X7)
| X2 != X7 )
| X0 = X1
| X0 = X2
| X1 = X2
| vf(X0,X1) != vf(X0,X2)
| ! [X3,X4,X5,X6] :
( ~ rpoint(X4)
| ~ rR(X1,X0,X3)
| ~ rpoint(X6)
| ~ rR(X2,X0,X5)
| X5 != X6
| X3 != X4
| vangle(X0,X1,X2) = vangle(X0,X2,X1) ) ),
inference(rectify,[],[f154]) ).
fof(f347,plain,
( rpoint(sK13)
& vd1361 = sK13 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X0,sK13)],[f14]) ).
fof(f360,plain,
! [X0,X1,X2,X3] :
( ~ rline(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ ron(X2,X0)
| ( rpoint(sK20(X0,X2))
& ron(sK20(X0,X2),X0)
& sK20(X0,X2) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X4,sK20(X0,X2))],[f206]) ).
fof(f364,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,[],[f212]) ).
fof(f365,plain,
! [X0,X1] :
( ! [X4] :
( ~ rpoint(X4)
| X0 != X4 )
| ! [X3] :
( ~ rpoint(X3)
| X1 != X3 )
| X0 = X1
| ( rline(sK23(X0,X1))
& ron(X0,sK23(X0,X1))
& ron(X1,sK23(X0,X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(X2,sK23(X0,X1))],[f364]) ).
fof(f406,plain,
vangle(vd1378,vd1363,vd1362) != vangle(vd1361,vd1362,vd1363),
inference(cnf_transformation,[],[f132]) ).
fof(f421,plain,
rpoint(vd1378),
inference(cnf_transformation,[],[f6]) ).
fof(f422,plain,
rR(vd1378,vd1361,vd1363),
inference(cnf_transformation,[],[f5]) ).
fof(f424,plain,
vf(vd1378,vd1363) = vf(vd1361,vd1362),
inference(cnf_transformation,[],[f3]) ).
fof(f428,plain,
vd1363 != vd1361,
inference(cnf_transformation,[],[f11]) ).
fof(f429,plain,
vd1363 != vd1362,
inference(cnf_transformation,[],[f10]) ).
fof(f430,plain,
vangle(vd1361,vd1362,vd1363) = vangle(vd1361,vd1363,vd1362),
inference(cnf_transformation,[],[f9]) ).
fof(f431,plain,
rpoint(sK5),
inference(cnf_transformation,[],[f336]) ).
fof(f432,plain,
vd1363 = sK5,
inference(cnf_transformation,[],[f336]) ).
fof(f433,plain,
rpoint(sK6),
inference(cnf_transformation,[],[f337]) ).
fof(f434,plain,
vd1362 = sK6,
inference(cnf_transformation,[],[f337]) ).
fof(f453,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,[],[f146]) ).
fof(f466,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ rpoint(X9)
| X0 != X9
| ~ rpoint(X8)
| X1 != X8
| ~ rpoint(X7)
| X2 != X7
| X0 = X1
| X0 = X2
| X1 = X2
| vf(X0,X1) != vf(X0,X2)
| ~ rpoint(X4)
| ~ rR(X1,X0,X3)
| ~ rpoint(X6)
| ~ rR(X2,X0,X5)
| X5 != X6
| X3 != X4
| vangle(X0,X1,X2) = vangle(X0,X2,X1) ),
inference(cnf_transformation,[],[f345]) ).
fof(f468,plain,
rpoint(sK13),
inference(cnf_transformation,[],[f347]) ).
fof(f469,plain,
vd1361 = sK13,
inference(cnf_transformation,[],[f347]) ).
fof(f484,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| X3 != X4
| ~ rR(X1,X0,X2)
| ~ rR(X3,X0,X1)
| rR(X3,X0,X2) ),
inference(cnf_transformation,[],[f168]) ).
fof(f485,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| X3 != X4
| ~ rR(X1,X0,X2)
| ~ rR(X1,X0,X3)
| ~ rR(X1,X2,X3) ),
inference(cnf_transformation,[],[f170]) ).
fof(f492,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X1,X0,X2)
| rR(X1,X2,X0) ),
inference(cnf_transformation,[],[f184]) ).
fof(f495,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,[],[f184]) ).
fof(f496,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,[],[f186]) ).
fof(f497,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| X3 != X4
| ~ rR(X1,X0,X2)
| ~ rR(X2,X1,X3)
| rR(X1,X0,X3) ),
inference(cnf_transformation,[],[f188]) ).
fof(f508,plain,
! [X2,X3,X0,X1] :
( ~ rline(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ ron(X2,X0)
| rpoint(sK20(X0,X2)) ),
inference(cnf_transformation,[],[f360]) ).
fof(f510,plain,
! [X2,X3,X0,X1] :
( ~ rline(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ ron(X2,X0)
| sK20(X0,X2) != X2 ),
inference(cnf_transformation,[],[f360]) ).
fof(f519,plain,
! [X3,X0,X1,X4] :
( ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X1 != X3
| X0 = X1
| rline(sK23(X0,X1)) ),
inference(cnf_transformation,[],[f365]) ).
fof(f520,plain,
! [X3,X0,X1,X4] :
( ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X1 != X3
| X0 = X1
| ron(X0,sK23(X0,X1)) ),
inference(cnf_transformation,[],[f365]) ).
fof(f521,plain,
! [X3,X0,X1,X4] :
( ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X1 != X3
| X0 = X1
| ron(X1,sK23(X0,X1)) ),
inference(cnf_transformation,[],[f365]) ).
fof(f656,plain,
vangle(vd1378,sK5,sK6) != vangle(sK13,sK6,sK5),
inference(definition_unfolding,[],[f406,f432,f434,f469,f434,f432]) ).
fof(f657,plain,
rR(vd1378,sK13,sK5),
inference(definition_unfolding,[],[f422,f469,f432]) ).
fof(f659,plain,
vf(sK13,sK6) = vf(vd1378,sK5),
inference(definition_unfolding,[],[f424,f432,f469,f434]) ).
fof(f663,plain,
sK5 != sK13,
inference(definition_unfolding,[],[f428,f432,f469]) ).
fof(f664,plain,
sK5 != sK6,
inference(definition_unfolding,[],[f429,f432,f434]) ).
fof(f665,plain,
vangle(sK13,sK6,sK5) = vangle(sK13,sK5,sK6),
inference(definition_unfolding,[],[f430,f469,f434,f432,f469,f432,f434]) ).
fof(f744,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,[],[f453]) ).
fof(f745,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,[],[f744]) ).
fof(f746,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,[],[f745]) ).
fof(f747,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,[],[f746]) ).
fof(f748,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,[],[f747]) ).
fof(f749,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,[],[f748]) ).
fof(f750,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,[],[f749]) ).
fof(f823,plain,
! [X2,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ rpoint(X9)
| X0 != X9
| ~ rpoint(X8)
| X1 != X8
| ~ rpoint(X7)
| X2 != X7
| X0 = X1
| X0 = X2
| X1 = X2
| vf(X0,X1) != vf(X0,X2)
| ~ rpoint(X4)
| ~ rR(X1,X0,X4)
| ~ rpoint(X6)
| ~ rR(X2,X0,X5)
| X5 != X6
| vangle(X0,X1,X2) = vangle(X0,X2,X1) ),
inference(equality_resolution,[],[f466]) ).
fof(f824,plain,
! [X2,X0,X1,X8,X6,X9,X7,X4] :
( ~ rpoint(X9)
| X0 != X9
| ~ rpoint(X8)
| X1 != X8
| ~ rpoint(X7)
| X2 != X7
| X0 = X1
| X0 = X2
| X1 = X2
| vf(X0,X1) != vf(X0,X2)
| ~ rpoint(X4)
| ~ rR(X1,X0,X4)
| ~ rpoint(X6)
| ~ rR(X2,X0,X6)
| vangle(X0,X1,X2) = vangle(X0,X2,X1) ),
inference(equality_resolution,[],[f823]) ).
fof(f825,plain,
! [X0,X1,X8,X6,X9,X7,X4] :
( ~ rpoint(X9)
| X0 != X9
| ~ rpoint(X8)
| X1 != X8
| ~ rpoint(X7)
| X0 = X1
| X0 = X7
| X1 = X7
| vf(X0,X1) != vf(X0,X7)
| ~ rpoint(X4)
| ~ rR(X1,X0,X4)
| ~ rpoint(X6)
| ~ rR(X7,X0,X6)
| vangle(X0,X1,X7) = vangle(X0,X7,X1) ),
inference(equality_resolution,[],[f824]) ).
fof(f826,plain,
! [X0,X8,X6,X9,X7,X4] :
( ~ rpoint(X9)
| X0 != X9
| ~ rpoint(X8)
| ~ rpoint(X7)
| X0 = X8
| X0 = X7
| X7 = X8
| vf(X0,X7) != vf(X0,X8)
| ~ rpoint(X4)
| ~ rR(X8,X0,X4)
| ~ rpoint(X6)
| ~ rR(X7,X0,X6)
| vangle(X0,X8,X7) = vangle(X0,X7,X8) ),
inference(equality_resolution,[],[f825]) ).
fof(f827,plain,
! [X8,X6,X9,X7,X4] :
( ~ rpoint(X9)
| ~ rpoint(X8)
| ~ rpoint(X7)
| X8 = X9
| X7 = X9
| X7 = X8
| vf(X9,X8) != vf(X9,X7)
| ~ rpoint(X4)
| ~ rR(X8,X9,X4)
| ~ rpoint(X6)
| ~ rR(X7,X9,X6)
| vangle(X9,X8,X7) = vangle(X9,X7,X8) ),
inference(equality_resolution,[],[f826]) ).
fof(f889,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| ~ rR(X1,X0,X2)
| ~ rR(X4,X0,X1)
| rR(X4,X0,X2) ),
inference(equality_resolution,[],[f484]) ).
fof(f890,plain,
! [X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rR(X1,X0,X5)
| ~ rR(X4,X0,X1)
| rR(X4,X0,X5) ),
inference(equality_resolution,[],[f889]) ).
fof(f891,plain,
! [X0,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rR(X6,X0,X5)
| ~ rR(X4,X0,X6)
| rR(X4,X0,X5) ),
inference(equality_resolution,[],[f890]) ).
fof(f892,plain,
! [X6,X7,X4,X5] :
( ~ rpoint(X7)
| ~ rpoint(X6)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rR(X6,X7,X5)
| ~ rR(X4,X7,X6)
| rR(X4,X7,X5) ),
inference(equality_resolution,[],[f891]) ).
fof(f893,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| ~ rR(X1,X0,X2)
| ~ rR(X1,X0,X4)
| ~ rR(X1,X2,X4) ),
inference(equality_resolution,[],[f485]) ).
fof(f894,plain,
! [X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rR(X1,X0,X5)
| ~ rR(X1,X0,X4)
| ~ rR(X1,X5,X4) ),
inference(equality_resolution,[],[f893]) ).
fof(f895,plain,
! [X0,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rR(X6,X0,X5)
| ~ rR(X6,X0,X4)
| ~ rR(X6,X5,X4) ),
inference(equality_resolution,[],[f894]) ).
fof(f896,plain,
! [X6,X7,X4,X5] :
( ~ rpoint(X7)
| ~ rpoint(X6)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rR(X6,X7,X5)
| ~ rR(X6,X7,X4)
| ~ rR(X6,X5,X4) ),
inference(equality_resolution,[],[f895]) ).
fof(f922,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,[],[f495]) ).
fof(f923,plain,
! [X3,X0,X4,X5] :
( ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rR(X4,X0,X3)
| ~ rR(X0,X4,X3) ),
inference(equality_resolution,[],[f922]) ).
fof(f924,plain,
! [X3,X4,X5] :
( ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rR(X4,X5,X3)
| ~ rR(X5,X4,X3) ),
inference(equality_resolution,[],[f923]) ).
fof(f933,plain,
! [X3,X0,X1,X4,X5] :
( ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| ~ rR(X1,X0,X3)
| rR(X1,X3,X0) ),
inference(equality_resolution,[],[f492]) ).
fof(f934,plain,
! [X3,X0,X4,X5] :
( ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rR(X4,X0,X3)
| rR(X4,X3,X0) ),
inference(equality_resolution,[],[f933]) ).
fof(f935,plain,
! [X3,X4,X5] :
( ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rR(X4,X5,X3)
| rR(X4,X3,X5) ),
inference(equality_resolution,[],[f934]) ).
fof(f936,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,[],[f496]) ).
fof(f937,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,[],[f936]) ).
fof(f938,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,[],[f937]) ).
fof(f939,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,[],[f938]) ).
fof(f940,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| ~ rR(X1,X0,X2)
| ~ rR(X2,X1,X4)
| rR(X1,X0,X4) ),
inference(equality_resolution,[],[f497]) ).
fof(f941,plain,
! [X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rR(X1,X0,X5)
| ~ rR(X5,X1,X4)
| rR(X1,X0,X4) ),
inference(equality_resolution,[],[f940]) ).
fof(f942,plain,
! [X0,X6,X7,X4,X5] :
( ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rR(X6,X0,X5)
| ~ rR(X5,X6,X4)
| rR(X6,X0,X4) ),
inference(equality_resolution,[],[f941]) ).
fof(f943,plain,
! [X6,X7,X4,X5] :
( ~ rpoint(X7)
| ~ rpoint(X6)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rR(X6,X7,X5)
| ~ rR(X5,X6,X4)
| rR(X6,X7,X4) ),
inference(equality_resolution,[],[f942]) ).
fof(f963,plain,
! [X3,X0,X1] :
( ~ rline(X1)
| X0 != X1
| ~ rpoint(X3)
| ~ ron(X3,X0)
| sK20(X0,X3) != X3 ),
inference(equality_resolution,[],[f510]) ).
fof(f964,plain,
! [X3,X1] :
( ~ rline(X1)
| ~ rpoint(X3)
| ~ ron(X3,X1)
| sK20(X1,X3) != X3 ),
inference(equality_resolution,[],[f963]) ).
fof(f967,plain,
! [X3,X0,X1] :
( ~ rline(X1)
| X0 != X1
| ~ rpoint(X3)
| ~ ron(X3,X0)
| rpoint(sK20(X0,X3)) ),
inference(equality_resolution,[],[f508]) ).
fof(f968,plain,
! [X3,X1] :
( ~ rline(X1)
| ~ rpoint(X3)
| ~ ron(X3,X1)
| rpoint(sK20(X1,X3)) ),
inference(equality_resolution,[],[f967]) ).
fof(f997,plain,
! [X3,X0,X4] :
( ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X0 = X3
| ron(X3,sK23(X0,X3)) ),
inference(equality_resolution,[],[f521]) ).
fof(f998,plain,
! [X3,X4] :
( ~ rpoint(X4)
| ~ rpoint(X3)
| X3 = X4
| ron(X3,sK23(X4,X3)) ),
inference(equality_resolution,[],[f997]) ).
fof(f999,plain,
! [X3,X0,X4] :
( ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X0 = X3
| ron(X0,sK23(X0,X3)) ),
inference(equality_resolution,[],[f520]) ).
fof(f1000,plain,
! [X3,X4] :
( ~ rpoint(X4)
| ~ rpoint(X3)
| X3 = X4
| ron(X4,sK23(X4,X3)) ),
inference(equality_resolution,[],[f999]) ).
fof(f1001,plain,
! [X3,X0,X4] :
( ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X0 = X3
| rline(sK23(X0,X3)) ),
inference(equality_resolution,[],[f519]) ).
fof(f1002,plain,
! [X3,X4] :
( ~ rpoint(X4)
| ~ rpoint(X3)
| X3 = X4
| rline(sK23(X4,X3)) ),
inference(equality_resolution,[],[f1001]) ).
tcf(c_49,negated_conjecture,
vangle(vd1378,sK5,sK6) != vangle(sK13,sK6,sK5),
inference(cnf_transformation,[],[f656]) ).
tcf(c_64,plain,
rpoint(vd1378),
inference(cnf_transformation,[],[f421]) ).
tcf(c_65,plain,
rR(vd1378,sK13,sK5),
inference(cnf_transformation,[],[f657]) ).
tcf(c_67,plain,
vf(vd1378,sK5) = vf(sK13,sK6),
inference(cnf_transformation,[],[f659]) ).
tcf(c_71,plain,
sK5 != sK13,
inference(cnf_transformation,[],[f663]) ).
tcf(c_72,plain,
sK5 != sK6,
inference(cnf_transformation,[],[f664]) ).
tcf(c_73,plain,
vangle(sK13,sK5,sK6) = vangle(sK13,sK6,sK5),
inference(cnf_transformation,[],[f665]) ).
tcf(c_74,plain,
rpoint(sK5),
inference(cnf_transformation,[],[f431]) ).
tcf(c_75,plain,
rpoint(sK6),
inference(cnf_transformation,[],[f433]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( rR(X6,X5,X2)
| rR(X6,X4,X0)
| ( X5 = X6 )
| ( X4 = X6 )
| ( X2 = X6 )
| ( X0 = X6 )
| ( vangle(X2,X6,X0) = vangle(X5,X6,X4) )
| ~ rline(X3)
| ~ rline(X1)
| ~ rpoint(X6)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ ron(X6,X3)
| ~ ron(X5,X3)
| ~ ron(X4,X1)
| ~ ron(X2,X3)
| ~ ron(X0,X1) ),
inference(cnf_transformation,[],[f750]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X1 = X2 )
| ( X0 = X2 )
| ( X0 = X1 )
| ( vangle(X0,X1,X2) = vangle(X0,X2,X1) )
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(X2,X0,X4)
| ~ rR(X1,X0,X3)
| ( vf(X0,X1) != vf(X0,X2) ) ),
inference(cnf_transformation,[],[f827]) ).
tcf(c_109,plain,
rpoint(sK13),
inference(cnf_transformation,[],[f468]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( rR(X0,X1,X3)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(X2,X1,X3)
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[],[f892]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(X0,X3,X2)
| ~ rR(X0,X3,X1)
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[],[f896]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(X1,X0,X2)
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[],[f924]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(X0,X1,X1) ),
inference(cnf_transformation,[],[f1397]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i,X2: $i] :
( rR(X0,X2,X1)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[],[f935]) ).
tcf(c_136,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,[],[f939]) ).
tcf(c_137,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( rR(X0,X1,X3)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(X2,X0,X3)
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[],[f943]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i] :
( ~ rline(X0)
| ~ rpoint(X1)
| ~ ron(X1,X0)
| ( sK20(X0,X1) != X1 ) ),
inference(cnf_transformation,[],[f964]) ).
tcf(c_150,plain,
! [X0: $i,X1: $i] :
( rpoint(sK20(X1,X0))
| ~ rline(X1)
| ~ rpoint(X0)
| ~ ron(X0,X1) ),
inference(cnf_transformation,[],[f968]) ).
tcf(c_159,plain,
! [X0: $i,X1: $i] :
( ron(X1,sK23(X0,X1))
| ( X0 = X1 )
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(cnf_transformation,[],[f998]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i] :
( ron(X0,sK23(X0,X1))
| ( X0 = X1 )
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(cnf_transformation,[],[f1000]) ).
tcf(c_161,plain,
! [X0: $i,X1: $i] :
( rline(sK23(X0,X1))
| ( X0 = X1 )
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(cnf_transformation,[],[f1002]) ).
tcf(c_3674,plain,
vangle(vd1378,sK5,sK6) != vangle(sK13,sK5,sK6),
inference(light_normalisation,[status(thm)],[c_49,c_73]) ).
tcf(c_15633,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_15635,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_23597,plain,
( rline(sK23(sK5,sK13))
| ( sK5 = sK13 )
| ~ rpoint(sK13)
| ~ rpoint(sK5) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_23598,plain,
( rline(sK23(sK5,sK6))
| ( sK5 = sK6 )
| ~ rpoint(sK6)
| ~ rpoint(sK5) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_23919,plain,
! [X0: $i] :
( ( sK5 = sK13 )
| ( sK13 != X0 )
| ( sK5 != X0 ) ),
inference(instantiation,[status(thm)],[c_15635]) ).
tcf(c_23920,plain,
! [X0: $i] :
( ( sK5 = sK6 )
| ( sK6 != X0 )
| ( sK5 != X0 ) ),
inference(instantiation,[status(thm)],[c_15635]) ).
tcf(c_24203,plain,
( ron(sK13,sK23(sK5,sK13))
| ( sK5 = sK13 )
| ~ rpoint(sK13)
| ~ rpoint(sK5) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_24204,plain,
( ron(sK6,sK23(sK5,sK6))
| ( sK5 = sK6 )
| ~ rpoint(sK6)
| ~ rpoint(sK5) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_24321,plain,
( ron(sK5,sK23(sK5,sK13))
| ( sK5 = sK13 )
| ~ rpoint(sK13)
| ~ rpoint(sK5) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_25473,plain,
( rR(vd1378,sK5,sK13)
| ~ rpoint(sK13)
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rR(vd1378,sK13,sK5) ),
inference(instantiation,[status(thm)],[c_135]) ).
tcf(c_26841,plain,
! [X0: $i] :
( rR(vd1378,sK13,X0)
| ~ rpoint(sK13)
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rpoint(X0)
| ~ rR(vd1378,sK13,sK5)
| ~ rR(sK5,sK13,X0) ),
inference(instantiation,[status(thm)],[c_124]) ).
tcf(c_26842,plain,
( rR(vd1378,sK13,sK13)
| ~ rpoint(sK13)
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rR(sK5,sK13,sK13)
| ~ rR(vd1378,sK13,sK5) ),
inference(instantiation,[status(thm)],[c_26841]) ).
tcf(c_26843,plain,
! [X0: $i] :
( ~ rpoint(sK13)
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rpoint(X0)
| ~ rR(vd1378,sK13,sK5)
| ~ rR(vd1378,X0,sK13)
| ~ rR(vd1378,X0,sK5) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_26844,plain,
( ~ rpoint(sK13)
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rR(vd1378,sK13,sK13)
| ~ rR(vd1378,sK13,sK5) ),
inference(instantiation,[status(thm)],[c_26843]) ).
tcf(c_39145,plain,
! [X0: $i] :
( ron(vd1378,X0)
| ~ rpoint(sK13)
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rline(X0)
| ~ ron(sK13,X0)
| ~ ron(sK5,X0) ),
inference(superposition,[status(thm)],[c_65,c_136]) ).
tcf(c_39147,plain,
! [X0: $i] :
( ron(vd1378,X0)
| ~ rline(X0)
| ~ ron(sK13,X0)
| ~ ron(sK5,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_39145,c_109,c_74,c_64]) ).
tcf(c_46396,plain,
! [X0: $i] :
( ron(vd1378,sK23(sK5,X0))
| ( X0 = sK5 )
| ~ rpoint(sK5)
| ~ rpoint(X0)
| ~ rline(sK23(sK5,X0))
| ~ ron(sK13,sK23(sK5,X0)) ),
inference(superposition,[status(thm)],[c_160,c_39147]) ).
tcf(c_46404,plain,
! [X0: $i] :
( ron(vd1378,sK23(sK5,X0))
| ( X0 = sK5 )
| ~ rpoint(X0)
| ~ rline(sK23(sK5,X0))
| ~ ron(sK13,sK23(sK5,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_46396,c_74]) ).
tcf(c_46417,plain,
( ron(vd1378,sK23(sK5,sK13))
| ( sK13 = sK5 )
| ~ rpoint(sK13)
| ~ rline(sK23(sK5,sK13))
| ~ ron(sK13,sK23(sK5,sK13)) ),
inference(instantiation,[status(thm)],[c_46404]) ).
tcf(c_46473,plain,
( ( sK5 = sK13 )
| ( sK13 != sK5 )
| ( sK5 != sK5 ) ),
inference(instantiation,[status(thm)],[c_23919]) ).
tcf(c_46474,plain,
sK5 = sK5,
inference(instantiation,[status(thm)],[c_15633]) ).
tcf(c_62635,plain,
( ( sK5 = sK6 )
| ( sK6 != sK5 )
| ( sK5 != sK5 ) ),
inference(instantiation,[status(thm)],[c_23920]) ).
tcf(c_180752,plain,
! [X0: $i] :
( rR(sK5,X0,sK13)
| ~ rpoint(sK13)
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rpoint(X0)
| ~ rR(vd1378,sK5,sK13)
| ~ rR(sK5,X0,vd1378) ),
inference(instantiation,[status(thm)],[c_137]) ).
tcf(c_180753,plain,
( rR(sK5,sK13,sK13)
| ~ rpoint(sK13)
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rR(sK5,sK13,vd1378)
| ~ rR(vd1378,sK5,sK13) ),
inference(instantiation,[status(thm)],[c_180752]) ).
tcf(c_344047,plain,
( ~ rpoint(sK6)
| ~ rline(sK23(sK5,sK6))
| ~ ron(sK6,sK23(sK5,sK6))
| ( sK20(sK23(sK5,sK6),sK6) != sK6 ) ),
inference(instantiation,[status(thm)],[c_148]) ).
tcf(c_362481,plain,
! [X0: $i,X1: $i] :
( rR(sK5,sK13,vd1378)
| rR(sK5,sK6,sK6)
| ( sK13 = sK5 )
| ( sK6 = sK5 )
| ( vd1378 = sK5 )
| ( vangle(vd1378,sK5,sK6) = vangle(sK13,sK5,sK6) )
| ~ rpoint(sK13)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rline(X1)
| ~ rline(X0)
| ~ ron(sK13,X0)
| ~ ron(sK6,X1)
| ~ ron(sK5,X0)
| ~ ron(vd1378,X0) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_362723,plain,
( rpoint(sK20(sK23(sK5,sK6),sK6))
| ~ rpoint(sK6)
| ~ rline(sK23(sK5,sK6))
| ~ ron(sK6,sK23(sK5,sK6)) ),
inference(instantiation,[status(thm)],[c_150]) ).
tcf(c_363503,plain,
! [X0: $i] :
( rR(sK5,sK13,vd1378)
| rR(sK5,sK6,sK6)
| ( sK13 = sK5 )
| ( sK6 = sK5 )
| ( vd1378 = sK5 )
| ( vangle(vd1378,sK5,sK6) = vangle(sK13,sK5,sK6) )
| ~ rpoint(sK13)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rline(X0)
| ~ ron(sK6,X0)
| ~ rline(sK23(sK5,sK13))
| ~ ron(sK13,sK23(sK5,sK13))
| ~ ron(sK5,sK23(sK5,sK13))
| ~ ron(vd1378,sK23(sK5,sK13)) ),
inference(instantiation,[status(thm)],[c_362481]) ).
tcf(c_364063,plain,
( ron(sK6,sK23(sK20(sK23(sK5,sK6),sK6),sK6))
| ( sK20(sK23(sK5,sK6),sK6) = sK6 )
| ~ rpoint(sK6)
| ~ rpoint(sK20(sK23(sK5,sK6),sK6)) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_364066,plain,
( rline(sK23(sK20(sK23(sK5,sK6),sK6),sK6))
| ( sK20(sK23(sK5,sK6),sK6) = sK6 )
| ~ rpoint(sK6)
| ~ rpoint(sK20(sK23(sK5,sK6),sK6)) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_365852,plain,
( rR(sK5,sK13,vd1378)
| rR(sK5,sK6,sK6)
| ( sK13 = sK5 )
| ( sK6 = sK5 )
| ( vd1378 = sK5 )
| ( vangle(vd1378,sK5,sK6) = vangle(sK13,sK5,sK6) )
| ~ rpoint(sK13)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rline(sK23(sK5,sK13))
| ~ ron(sK13,sK23(sK5,sK13))
| ~ ron(sK5,sK23(sK5,sK13))
| ~ ron(vd1378,sK23(sK5,sK13))
| ~ rline(sK23(sK20(sK23(sK5,sK6),sK6),sK6))
| ~ ron(sK6,sK23(sK20(sK23(sK5,sK6),sK6),sK6)) ),
inference(instantiation,[status(thm)],[c_363503]) ).
tcf(c_375594,plain,
( ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rR(sK5,sK6,sK6) ),
inference(instantiation,[status(thm)],[c_133]) ).
tcf(c_384023,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( vd1378 = sK5 )
| ( X0 = sK5 )
| ( X0 = vd1378 )
| ( vangle(vd1378,X0,sK5) = vangle(vd1378,sK5,X0) )
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(sK5,vd1378,X2)
| ~ rR(X0,vd1378,X1)
| ( vf(vd1378,X0) != vf(sK13,sK6) ) ),
inference(superposition,[status(thm)],[c_67,c_107]) ).
tcf(c_384027,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( vd1378 = sK5 )
| ( X0 = sK5 )
| ( X0 = vd1378 )
| ( vangle(vd1378,X0,sK5) = vangle(vd1378,sK5,X0) )
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(sK5,vd1378,X2)
| ~ rR(X0,vd1378,X1)
| ( vf(vd1378,X0) != vf(sK13,sK6) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_384023,c_74,c_64]) ).
tcf(c_384852,plain,
( rR(vd1378,sK5,sK13)
| ~ rpoint(sK13)
| ~ rpoint(sK5)
| ~ rpoint(vd1378) ),
inference(superposition,[status(thm)],[c_65,c_135]) ).
tcf(c_384853,plain,
rR(vd1378,sK5,sK13),
inference(forward_subsumption_resolution,[status(thm)],[c_384852,c_109,c_74,c_64]) ).
tcf(c_384878,plain,
( ~ rpoint(sK13)
| ~ rpoint(sK5)
| ~ rpoint(vd1378)
| ~ rR(sK5,vd1378,sK13) ),
inference(superposition,[status(thm)],[c_384853,c_132]) ).
tcf(c_384885,plain,
~ rR(sK5,vd1378,sK13),
inference(forward_subsumption_resolution,[status(thm)],[c_384878,c_109,c_74,c_64]) ).
tcf(c_437299,plain,
vd1378 = sK5,
inference(global_subsumption_just,[status(thm)],[c_384027,c_109,c_75,c_74,c_64,c_65,c_72,c_71,c_3674,c_23597,c_23598,c_24203,c_24204,c_24321,c_25473,c_26842,c_26844,c_46417,c_46473,c_46474,c_62635,c_180753,c_344047,c_362723,c_364066,c_364063,c_365852,c_375594]) ).
tcf(c_437355,plain,
~ rR(sK5,sK5,sK13),
inference(demodulation,[status(thm)],[c_384885,c_437299]) ).
tcf(c_437357,plain,
rR(sK5,sK5,sK13),
inference(demodulation,[status(thm)],[c_384853,c_437299]) ).
tcf(c_437366,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_437355,c_437357]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO337+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.09/0.36 % Computer : n010.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.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 11:58:42 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 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.41 % Detected problem language: tptp
% 0.10/0.42 % Proving...
% 130.09/31.47 % SZS status Started for theBenchmark.p
% 130.09/31.47 % SZS status Theorem for theBenchmark.p
% 130.09/31.47
% 130.09/31.47 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 130.09/31.47
% 130.09/31.47 % ------ iProver source info
% 130.09/31.47
% 130.09/31.47 % git: date: 2026-07-19 20:42:38 +0200
% 130.09/31.47 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 130.09/31.47 % git: non_committed_changes: false
% 130.09/31.47
% 130.09/31.47 % ------ Parsing...
% 130.09/31.47 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 130.09/31.47
% 130.09/31.47 % ------ 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 %
% 130.09/31.47
% 130.09/31.47 % ------ Preprocessing... gs_s sp: 12 0s gs_e snvd_s sp: 0 0s snvd_e %
% 130.09/31.47
% 130.09/31.47 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 130.09/31.47 % ------ Proving...
% 130.09/31.47 % ------ Problem Properties
% 130.09/31.47
% 130.09/31.47 %
% 130.09/31.47 % clauses 251
% 130.09/31.47 % conjectures 0
% 130.09/31.47 % EPR 57
% 130.09/31.47 % Horn 168
% 130.09/31.47 % unary 15
% 130.09/31.47 % binary 40
% 130.09/31.47 % lits 1577
% 130.09/31.47 % lits eq 254
% 130.09/31.47 % fd_pure 0
% 130.09/31.47 % fd_pseudo 0
% 130.09/31.47 % fd_cond 0
% 130.09/31.47 % fd_pseudo_cond 54
% 130.09/31.47 % AC symbols 0
% 130.09/31.47
% 130.09/31.47 % ------ Schedule dynamic 5 is on
% 130.09/31.47
% 130.09/31.47 % ------ no conjectures: strip conj schedule
% 130.09/31.47
% 130.09/31.47 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 130.09/31.47
% 130.09/31.47
% 130.09/31.47 % ------
% 130.09/31.47 % Current options:
% 130.09/31.47 % ------
% 130.09/31.47
% 130.09/31.47
% 130.09/31.47 %
% 130.09/31.47
% 130.09/31.47 % ------ Proving...
% 130.09/31.47 % Proof_search_loop: time out after: 4484 full_loop iterations
% 130.09/31.47
% 130.09/31.47 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" stripped conjectures Time Limit: 15.
% 130.09/31.47
% 130.09/31.47
% 130.09/31.47 % ------
% 130.09/31.47 % Current options:
% 130.09/31.47 % ------
% 130.09/31.47
% 130.09/31.47
% 130.09/31.47 %
% 130.09/31.47
% 130.09/31.47 % ------ Proving...
% 130.09/31.47 % Proof_search_loop: time out after: 10369 full_loop iterations
% 130.09/31.47
% 130.09/31.47 % ------ Option_1: Negative Selections stripped conjectures Time Limit: 35.
% 130.09/31.47
% 130.09/31.47
% 130.09/31.47 % ------
% 130.09/31.47 % Current options:
% 130.09/31.47 % ------
% 130.09/31.47
% 130.09/31.47
% 130.09/31.47 %
% 130.09/31.47
% 130.09/31.47 % ------ Proving...
% 130.09/31.47 %
% 130.09/31.47
% 130.09/31.47 % SZS status Theorem for theBenchmark.p
% 130.09/31.47
% 130.09/31.47 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 130.09/31.47
% 130.09/31.47
%------------------------------------------------------------------------------