%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO317+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 : Tue Sep 29 09:52:26 AM UTC 2026
% Result : Theorem 38.27s 6.24s
% Output : Refutation 38.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 57
% Syntax : Number of formulae : 664 ( 114 unt; 23 def)
% Number of atoms : 3890 (1224 equ)
% Maximal formula atoms : 26 ( 5 avg)
% Number of connectives : 5589 (2363 ~;3018 |; 168 &)
% ( 27 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 22 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 17 con; 0-3 aty)
% Number of variables : 1220 ( 0 sgn1173 !; 47 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vangle(vd1287,vd1289,vd1288) = vangle(vd1287,vd1288,vd1289),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(364, 1327, 0)') ).
fof(f2,negated_conjecture,
vangle(vd1287,vd1289,vd1288) != vangle(vd1287,vd1288,vd1289),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f9,axiom,
vf(vd1299,vd1289) = vf(vd1288,vd1306),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(360), 1321, 0)') ).
fof(f15,axiom,
rpoint(vd1306),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(352, 0)') ).
fof(f16,axiom,
( vf(vd1287,vd1288) = vf(vd1287,vd1289)
& vd1288 != vd1289
& vd1287 != vd1289
& vd1287 != vd1288
& ? [X0] :
( vd1289 = X0
& rpoint(X0) )
& ? [X1] :
( vd1288 = X1
& rpoint(X1) )
& ? [X2] :
( vd1287 = X2
& rpoint(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))') ).
fof(f17,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( ~ rR(X0,X2,X4)
& ~ rR(X0,X1,X3)
& X4 != X0
& X3 != X0
& X2 != X0
& X1 != X0
& ron(X4,X6)
& ron(X2,X6)
& ron(X3,X5)
& ron(X1,X5)
& ron(X0,X5)
& ? [X7] :
( X6 = X7
& rline(X7) )
& ? [X8] :
( X5 = X8
& rline(X8) )
& ? [X9] :
( X4 = X9
& rpoint(X9) )
& ? [X10] :
( X3 = X10
& rpoint(X10) )
& ? [X11] :
( X2 = X11
& rpoint(X11) )
& ? [X12] :
( X1 = X12
& rpoint(X12) )
& ? [X13] :
( X0 = X13
& rpoint(X13) ) )
=> vangle(X1,X0,X2) = vangle(X3,X0,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))') ).
fof(f20,axiom,
vangle(vd1288,vd1287,vd1289) = vangle(vd1299,vd1287,vd1289),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(358, 1317, 0)') ).
fof(f21,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ron(X2,X6)
& ron(X0,X6)
& X0 != X4
& X0 != X2
& X6 = X7
& rline(X7)
& X4 = X5
& rpoint(X5)
& X2 = X3
& rpoint(X3)
& X0 = X1
& rpoint(X1) )
=> ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
<=> vangle(X2,X0,X4) = v0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(188), 0), imp(cond(axiom(188), 0)))') ).
fof(f24,axiom,
rR(vd1306,vd1287,vd1302),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(352), 1307, 0)') ).
fof(f30,axiom,
ron(vd1302,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct2(349), 0)') ).
fof(f36,axiom,
( vd1302 = vd1303
& rR(vd1289,vd1287,vd1302)
& rpoint(vd1303)
& rR(vd1288,vd1287,vd1299) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))') ).
fof(f39,axiom,
rline(vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(347, 0)') ).
fof(f42,axiom,
rline(vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(346, 0)') ).
fof(f47,axiom,
! [X0,X1,X2] :
( ( X0 != X2
& X0 != X1
& ? [X3] :
( X2 = X3
& rpoint(X3) )
& ? [X4] :
( X1 = X4
& rpoint(X4) )
& ? [X5] :
( X0 = X5
& rpoint(X5) ) )
=> vangle(X0,X1,X2) = vangle(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(168), 0), imp(cond(axiom(168), 0)))') ).
fof(f49,axiom,
! [X0,X1,X2,X3] :
( ( rR(X2,X1,X3)
& rR(X1,X0,X2)
& ? [X4] :
( X3 = X4
& rpoint(X4) )
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> rR(X1,X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(89), 0), imp(cond(axiom(89), 0)))') ).
fof(f51,axiom,
! [X0,X1,X2] :
( ( rR(X1,X0,X2)
& ? [X3] :
( X2 = X3
& rpoint(X3) )
& ? [X4] :
( X1 = X4
& rpoint(X4) )
& ? [X5] :
( X0 = X5
& rpoint(X5) ) )
=> ( ~ rR(X0,X1,X2)
& X0 != X2
& X0 != X1
& rR(X1,X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))') ).
fof(f54,axiom,
vd1289 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(355)), 1313, 0)') ).
fof(f55,axiom,
vd1288 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(355), 1312, 0)') ).
fof(f56,axiom,
ron(vd1289,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(354))))), 0)') ).
fof(f57,axiom,
ron(vd1288,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(354))))), 0)') ).
fof(f59,axiom,
ron(vd1287,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(conjunct2(354))), 0)') ).
fof(f60,axiom,
ron(vd1299,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(354)), 0)') ).
fof(f61,axiom,
ron(vd1287,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(354), 0)') ).
fof(f62,axiom,
vd1299 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(conjunct2(conjunct2(353))), 1311, 0)') ).
fof(f66,axiom,
vd1299 = vd1300,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(348, 4)') ).
fof(f67,axiom,
rpoint(vd1300),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(348, 1)') ).
fof(f69,axiom,
! [X0,X1] :
( ( ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ( vf(X0,X1) = v0
<=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))') ).
fof(f70,axiom,
! [X0,X1] :
( ( X0 != X1
& ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ? [X4] :
( ron(X1,X4)
& ron(X0,X4)
& rline(X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(51), 0), imp(cond(axiom(51), 0)))') ).
fof(f81,axiom,
! [X0,X1,X2,X3,X4] :
( ( vf(X2,X0) = vf(X2,X1)
& ron(X1,X4)
& ron(X0,X3)
& rcenter(X2,X4)
& rcenter(X2,X3)
& ? [X5] :
( X1 = X5
& rpoint(X5) )
& ? [X6] :
( X0 = X6
& rpoint(X6) ) )
=> X3 = X4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))') ).
fof(f85,axiom,
v0 = vd684,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(axiom(137), 2)') ).
fof(f92,axiom,
! [X0,X1] :
( ( X0 != X1
& ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ? [X4] :
( ron(X1,X4)
& rcenter(X0,X4)
& rcircle(X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(53), 0), imp(cond(axiom(53), 0)))') ).
fof(f106,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( X1 != X2
& ron(X2,X5)
& ron(X1,X5)
& rinside(X0,X5)
& ron(X2,X3)
& ron(X1,X3)
& ron(X0,X3)
& X5 = X6
& rcircle(X6)
& X3 = X4
& rline(X4)
& ? [X7] :
( X2 = X7
& rpoint(X7) )
& ? [X8] :
( X1 = X8
& rpoint(X8) )
& ? [X9] :
( X0 = X9
& rpoint(X9) ) )
=> rR(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(119), 0), imp(cond(axiom(119), 0)))') ).
fof(f116,axiom,
! [X0,X1,X2,X3] :
( ( rR(X1,X0,X3)
& rR(X1,X0,X2)
& ? [X4] :
( X3 = X4
& rpoint(X4) )
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ~ rR(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(93), 0), imp(cond(axiom(93), 0)))') ).
fof(f117,axiom,
! [X0,X1,X2,X3] :
( ( rR(X3,X0,X1)
& rR(X1,X0,X2)
& ? [X4] :
( X3 = X4
& rpoint(X4) )
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> rR(X3,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(87), 0), imp(cond(axiom(87), 0)))') ).
fof(f118,axiom,
! [X0,X1] :
( rcenter(X0,X1)
=> rinside(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))') ).
fof(f159,plain,
vangle(vd1287,vd1289,vd1288) != vangle(vd1287,vd1288,vd1289),
inference(flattening,[],[f2]) ).
fof(f172,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( vangle(X1,X0,X2) = vangle(X3,X0,X4)
| rR(X0,X2,X4)
| rR(X0,X1,X3)
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| ~ ron(X4,X6)
| ~ ron(X2,X6)
| ~ ron(X3,X5)
| ~ ron(X1,X5)
| ~ ron(X0,X5)
| ! [X7] :
( X6 != X7
| ~ rline(X7) )
| ! [X8] :
( X5 != X8
| ~ rline(X8) )
| ! [X9] :
( X4 != X9
| ~ rpoint(X9) )
| ! [X10] :
( X3 != X10
| ~ rpoint(X10) )
| ! [X11] :
( X2 != X11
| ~ rpoint(X11) )
| ! [X12] :
( X1 != X12
| ~ rpoint(X12) )
| ! [X13] :
( X0 != X13
| ~ rpoint(X13) ) ),
inference(ennf_transformation,[],[f17]) ).
fof(f173,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( vangle(X1,X0,X2) = vangle(X3,X0,X4)
| rR(X0,X2,X4)
| rR(X0,X1,X3)
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| ~ ron(X4,X6)
| ~ ron(X2,X6)
| ~ ron(X3,X5)
| ~ ron(X1,X5)
| ~ ron(X0,X5)
| ! [X7] :
( X6 != X7
| ~ rline(X7) )
| ! [X8] :
( X5 != X8
| ~ rline(X8) )
| ! [X9] :
( X4 != X9
| ~ rpoint(X9) )
| ! [X10] :
( X3 != X10
| ~ rpoint(X10) )
| ! [X11] :
( X2 != X11
| ~ rpoint(X11) )
| ! [X12] :
( X1 != X12
| ~ rpoint(X12) )
| ! [X13] :
( X0 != X13
| ~ rpoint(X13) ) ),
inference(flattening,[],[f172]) ).
fof(f176,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
<=> vangle(X2,X0,X4) = v0 )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f177,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
<=> vangle(X2,X0,X4) = v0 )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(flattening,[],[f176]) ).
fof(f198,plain,
! [X0,X1,X2] :
( vangle(X0,X1,X2) = vangle(X2,X1,X0)
| X0 = X2
| X0 = X1
| ! [X3] :
( X2 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(ennf_transformation,[],[f47]) ).
fof(f199,plain,
! [X0,X1,X2] :
( vangle(X0,X1,X2) = vangle(X2,X1,X0)
| X0 = X2
| X0 = X1
| ! [X3] :
( X2 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(flattening,[],[f198]) ).
fof(f202,plain,
! [X0,X1,X2,X3] :
( rR(X1,X0,X3)
| ~ rR(X2,X1,X3)
| ~ rR(X1,X0,X2)
| ! [X4] :
( X3 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f49]) ).
fof(f203,plain,
! [X0,X1,X2,X3] :
( rR(X1,X0,X3)
| ~ rR(X2,X1,X3)
| ~ rR(X1,X0,X2)
| ! [X4] :
( X3 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f202]) ).
fof(f206,plain,
! [X0,X1,X2] :
( ( ~ rR(X0,X1,X2)
& X0 != X2
& X0 != X1
& rR(X1,X2,X0) )
| ~ rR(X1,X0,X2)
| ! [X3] :
( X2 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(ennf_transformation,[],[f51]) ).
fof(f207,plain,
! [X0,X1,X2] :
( ( ~ rR(X0,X1,X2)
& X0 != X2
& X0 != X1
& rR(X1,X2,X0) )
| ~ rR(X1,X0,X2)
| ! [X3] :
( X2 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(flattening,[],[f206]) ).
fof(f210,plain,
! [X0,X1] :
( ( vf(X0,X1) = v0
<=> X0 = X1 )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f69]) ).
fof(f211,plain,
! [X0,X1] :
( ( vf(X0,X1) = v0
<=> X0 = X1 )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f210]) ).
fof(f212,plain,
! [X0,X1] :
( ? [X4] :
( ron(X1,X4)
& ron(X0,X4)
& rline(X4) )
| X0 = X1
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f70]) ).
fof(f213,plain,
! [X0,X1] :
( ? [X4] :
( ron(X1,X4)
& ron(X0,X4)
& rline(X4) )
| X0 = X1
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f212]) ).
fof(f232,plain,
! [X0,X1,X2,X3,X4] :
( X3 = X4
| vf(X2,X0) != vf(X2,X1)
| ~ ron(X1,X4)
| ~ ron(X0,X3)
| ~ rcenter(X2,X4)
| ~ rcenter(X2,X3)
| ! [X5] :
( X1 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X0 != X6
| ~ rpoint(X6) ) ),
inference(ennf_transformation,[],[f81]) ).
fof(f233,plain,
! [X0,X1,X2,X3,X4] :
( X3 = X4
| vf(X2,X0) != vf(X2,X1)
| ~ ron(X1,X4)
| ~ ron(X0,X3)
| ~ rcenter(X2,X4)
| ~ rcenter(X2,X3)
| ! [X5] :
( X1 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X0 != X6
| ~ rpoint(X6) ) ),
inference(flattening,[],[f232]) ).
fof(f250,plain,
! [X0,X1] :
( ? [X4] :
( ron(X1,X4)
& rcenter(X0,X4)
& rcircle(X4) )
| X0 = X1
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f92]) ).
fof(f251,plain,
! [X0,X1] :
( ? [X4] :
( ron(X1,X4)
& rcenter(X0,X4)
& rcircle(X4) )
| X0 = X1
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f250]) ).
fof(f277,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( rR(X0,X1,X2)
| X1 = X2
| ~ ron(X2,X5)
| ~ ron(X1,X5)
| ~ rinside(X0,X5)
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| X5 != X6
| ~ rcircle(X6)
| X3 != X4
| ~ rline(X4)
| ! [X7] :
( X2 != X7
| ~ rpoint(X7) )
| ! [X8] :
( X1 != X8
| ~ rpoint(X8) )
| ! [X9] :
( X0 != X9
| ~ rpoint(X9) ) ),
inference(ennf_transformation,[],[f106]) ).
fof(f278,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( rR(X0,X1,X2)
| X1 = X2
| ~ ron(X2,X5)
| ~ ron(X1,X5)
| ~ rinside(X0,X5)
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| X5 != X6
| ~ rcircle(X6)
| X3 != X4
| ~ rline(X4)
| ! [X7] :
( X2 != X7
| ~ rpoint(X7) )
| ! [X8] :
( X1 != X8
| ~ rpoint(X8) )
| ! [X9] :
( X0 != X9
| ~ rpoint(X9) ) ),
inference(flattening,[],[f277]) ).
fof(f297,plain,
! [X0,X1,X2,X3] :
( ~ rR(X1,X2,X3)
| ~ rR(X1,X0,X3)
| ~ rR(X1,X0,X2)
| ! [X4] :
( X3 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f116]) ).
fof(f298,plain,
! [X0,X1,X2,X3] :
( ~ rR(X1,X2,X3)
| ~ rR(X1,X0,X3)
| ~ rR(X1,X0,X2)
| ! [X4] :
( X3 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f297]) ).
fof(f299,plain,
! [X0,X1,X2,X3] :
( rR(X3,X0,X2)
| ~ rR(X3,X0,X1)
| ~ rR(X1,X0,X2)
| ! [X4] :
( X3 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f117]) ).
fof(f300,plain,
! [X0,X1,X2,X3] :
( rR(X3,X0,X2)
| ~ rR(X3,X0,X1)
| ~ rR(X1,X0,X2)
| ! [X4] :
( X3 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f299]) ).
fof(f301,plain,
! [X0,X1] :
( rinside(X0,X1)
| ~ rcenter(X0,X1) ),
inference(ennf_transformation,[],[f118]) ).
fof(f381,plain,
( vf(vd1287,vd1288) = vf(vd1287,vd1289)
& vd1288 != vd1289
& vd1287 != vd1289
& vd1287 != vd1288
& vd1289 = sK4
& rpoint(sK4)
& vd1288 = sK5
& rpoint(sK5)
& vd1287 = sK6
& rpoint(sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6)],[f16]) ).
fof(f382,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
| vangle(X2,X0,X4) != v0 )
& ( vangle(X2,X0,X4) = v0
| rR(X0,X2,X4)
| ~ ron(X4,X6) ) )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(nnf_transformation,[],[f177]) ).
fof(f383,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
| vangle(X2,X0,X4) != v0 )
& ( vangle(X2,X0,X4) = v0
| rR(X0,X2,X4)
| ~ ron(X4,X6) ) )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(flattening,[],[f382]) ).
fof(f389,plain,
! [X0,X1] :
( ( ( vf(X0,X1) = v0
| X0 != X1 )
& ( X0 = X1
| vf(X0,X1) != v0 ) )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(nnf_transformation,[],[f211]) ).
fof(f390,plain,
! [X0,X1] :
( ? [X2] :
( ron(X1,X2)
& ron(X0,X2)
& rline(X2) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(rectify,[],[f213]) ).
fof(f391,plain,
! [X0,X1] :
( ( ron(X1,sK7(X0,X1))
& ron(X0,sK7(X0,X1))
& rline(sK7(X0,X1)) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f390]) ).
fof(f401,plain,
! [X0,X1] :
( ? [X2] :
( ron(X1,X2)
& rcenter(X0,X2)
& rcircle(X2) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(rectify,[],[f251]) ).
fof(f402,plain,
! [X0,X1] :
( ( ron(X1,sK15(X0,X1))
& rcenter(X0,sK15(X0,X1))
& rcircle(sK15(X0,X1)) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X2,sK15(X0,X1))],[f401]) ).
fof(f452,plain,
vangle(vd1287,vd1289,vd1288) != vangle(vd1287,vd1288,vd1289),
inference(cnf_transformation,[],[f159]) ).
fof(f461,plain,
vf(vd1299,vd1289) = vf(vd1288,vd1306),
inference(cnf_transformation,[],[f9]) ).
fof(f476,plain,
rpoint(vd1306),
inference(cnf_transformation,[],[f15]) ).
fof(f477,plain,
rpoint(sK6),
inference(cnf_transformation,[],[f381]) ).
fof(f478,plain,
vd1287 = sK6,
inference(cnf_transformation,[],[f381]) ).
fof(f479,plain,
rpoint(sK5),
inference(cnf_transformation,[],[f381]) ).
fof(f480,plain,
vd1288 = sK5,
inference(cnf_transformation,[],[f381]) ).
fof(f481,plain,
rpoint(sK4),
inference(cnf_transformation,[],[f381]) ).
fof(f482,plain,
vd1289 = sK4,
inference(cnf_transformation,[],[f381]) ).
fof(f485,plain,
vd1289 != vd1288,
inference(cnf_transformation,[],[f381]) ).
fof(f486,plain,
vf(vd1287,vd1288) = vf(vd1287,vd1289),
inference(cnf_transformation,[],[f381]) ).
fof(f487,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( vangle(X1,X0,X2) = vangle(X3,X0,X4)
| rR(X0,X2,X4)
| rR(X0,X1,X3)
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| ~ ron(X4,X6)
| ~ ron(X2,X6)
| ~ ron(X3,X5)
| ~ ron(X1,X5)
| ~ ron(X0,X5)
| X6 != X7
| ~ rline(X7)
| X5 != X8
| ~ rline(X8)
| X4 != X9
| ~ rpoint(X9)
| X3 != X10
| ~ rpoint(X10)
| X2 != X11
| ~ rpoint(X11)
| X1 != X12
| ~ rpoint(X12)
| X0 != X13
| ~ rpoint(X13) ),
inference(cnf_transformation,[],[f173]) ).
fof(f490,plain,
vangle(vd1288,vd1287,vd1289) = vangle(vd1299,vd1287,vd1289),
inference(cnf_transformation,[],[f20]) ).
fof(f491,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( vangle(X2,X0,X4) = v0
| rR(X0,X2,X4)
| ~ ron(X4,X6)
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f383]) ).
fof(f492,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X4,X6)
| vangle(X2,X0,X4) != v0
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f383]) ).
fof(f493,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rR(X0,X2,X4)
| vangle(X2,X0,X4) != v0
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f383]) ).
fof(f496,plain,
rR(vd1306,vd1287,vd1302),
inference(cnf_transformation,[],[f24]) ).
fof(f502,plain,
ron(vd1302,vd1297),
inference(cnf_transformation,[],[f30]) ).
fof(f509,plain,
rR(vd1288,vd1287,vd1299),
inference(cnf_transformation,[],[f36]) ).
fof(f510,plain,
rpoint(vd1303),
inference(cnf_transformation,[],[f36]) ).
fof(f511,plain,
rR(vd1289,vd1287,vd1302),
inference(cnf_transformation,[],[f36]) ).
fof(f512,plain,
vd1302 = vd1303,
inference(cnf_transformation,[],[f36]) ).
fof(f515,plain,
rline(vd1297),
inference(cnf_transformation,[],[f39]) ).
fof(f518,plain,
rline(vd1295),
inference(cnf_transformation,[],[f42]) ).
fof(f524,plain,
! [X2,X3,X0,X1,X4,X5] :
( vangle(X0,X1,X2) = vangle(X2,X1,X0)
| X0 = X2
| X0 = X1
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(cnf_transformation,[],[f199]) ).
fof(f526,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( rR(X1,X0,X3)
| ~ rR(X2,X1,X3)
| ~ rR(X1,X0,X2)
| X3 != X4
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f203]) ).
fof(f528,plain,
! [X2,X3,X0,X1,X4,X5] :
( rR(X1,X2,X0)
| ~ rR(X1,X0,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(cnf_transformation,[],[f207]) ).
fof(f529,plain,
! [X2,X3,X0,X1,X4,X5] :
( X0 != X1
| ~ rR(X1,X0,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(cnf_transformation,[],[f207]) ).
fof(f530,plain,
! [X2,X3,X0,X1,X4,X5] :
( X0 != X2
| ~ rR(X1,X0,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(cnf_transformation,[],[f207]) ).
fof(f531,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ rR(X0,X1,X2)
| ~ rR(X1,X0,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(cnf_transformation,[],[f207]) ).
fof(f534,plain,
vd1287 != vd1289,
inference(cnf_transformation,[],[f54]) ).
fof(f535,plain,
vd1287 != vd1288,
inference(cnf_transformation,[],[f55]) ).
fof(f536,plain,
ron(vd1289,vd1297),
inference(cnf_transformation,[],[f56]) ).
fof(f537,plain,
ron(vd1288,vd1295),
inference(cnf_transformation,[],[f57]) ).
fof(f539,plain,
ron(vd1287,vd1297),
inference(cnf_transformation,[],[f59]) ).
fof(f540,plain,
ron(vd1299,vd1295),
inference(cnf_transformation,[],[f60]) ).
fof(f541,plain,
ron(vd1287,vd1295),
inference(cnf_transformation,[],[f61]) ).
fof(f542,plain,
vd1287 != vd1299,
inference(cnf_transformation,[],[f62]) ).
fof(f546,plain,
vd1299 = vd1300,
inference(cnf_transformation,[],[f66]) ).
fof(f547,plain,
rpoint(vd1300),
inference(cnf_transformation,[],[f67]) ).
fof(f550,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| vf(X0,X1) != v0
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f389]) ).
fof(f551,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = v0
| X0 != X1
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f389]) ).
fof(f552,plain,
! [X3,X0,X1,X4] :
( rline(sK7(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f391]) ).
fof(f553,plain,
! [X3,X0,X1,X4] :
( ron(X0,sK7(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f391]) ).
fof(f554,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK7(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f391]) ).
fof(f580,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( X3 = X4
| vf(X2,X0) != vf(X2,X1)
| ~ ron(X1,X4)
| ~ ron(X0,X3)
| ~ rcenter(X2,X4)
| ~ rcenter(X2,X3)
| X1 != X5
| ~ rpoint(X5)
| X0 != X6
| ~ rpoint(X6) ),
inference(cnf_transformation,[],[f233]) ).
fof(f584,plain,
v0 = vd684,
inference(cnf_transformation,[],[f85]) ).
fof(f601,plain,
! [X3,X0,X1,X4] :
( rcircle(sK15(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f402]) ).
fof(f602,plain,
! [X3,X0,X1,X4] :
( rcenter(X0,sK15(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f402]) ).
fof(f603,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK15(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f402]) ).
fof(f631,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( rR(X0,X1,X2)
| X1 = X2
| ~ ron(X2,X5)
| ~ ron(X1,X5)
| ~ rinside(X0,X5)
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| X5 != X6
| ~ rcircle(X6)
| X3 != X4
| ~ rline(X4)
| X2 != X7
| ~ rpoint(X7)
| X1 != X8
| ~ rpoint(X8)
| X0 != X9
| ~ rpoint(X9) ),
inference(cnf_transformation,[],[f278]) ).
fof(f641,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rR(X1,X2,X3)
| ~ rR(X1,X0,X3)
| ~ rR(X1,X0,X2)
| X3 != X4
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f298]) ).
fof(f642,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( rR(X3,X0,X2)
| ~ rR(X3,X0,X1)
| ~ rR(X1,X0,X2)
| X3 != X4
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f300]) ).
fof(f643,plain,
! [X0,X1] :
( ~ rcenter(X0,X1)
| rinside(X0,X1) ),
inference(cnf_transformation,[],[f301]) ).
fof(f753,plain,
vangle(sK6,sK4,sK5) != vangle(sK6,sK5,sK4),
inference(definition_unfolding,[],[f452,f478,f482,f480,f478,f480,f482]) ).
fof(f759,plain,
vf(vd1300,sK4) = vf(sK5,vd1306),
inference(definition_unfolding,[],[f461,f546,f482,f480]) ).
fof(f762,plain,
vf(sK6,sK5) = vf(sK6,sK4),
inference(definition_unfolding,[],[f486,f478,f480,f478,f482]) ).
fof(f763,plain,
sK4 != sK5,
inference(definition_unfolding,[],[f485,f482,f480]) ).
fof(f767,plain,
vangle(sK5,sK6,sK4) = vangle(vd1300,sK6,sK4),
inference(definition_unfolding,[],[f490,f480,f478,f482,f546,f478,f482]) ).
fof(f768,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rR(X0,X2,X4)
| vangle(X2,X0,X4) != vd684
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(definition_unfolding,[],[f493,f584]) ).
fof(f769,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X4,X6)
| vangle(X2,X0,X4) != vd684
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(definition_unfolding,[],[f492,f584]) ).
fof(f770,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( vangle(X2,X0,X4) = vd684
| rR(X0,X2,X4)
| ~ ron(X4,X6)
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(definition_unfolding,[],[f491,f584]) ).
fof(f773,plain,
rR(vd1306,sK6,vd1303),
inference(definition_unfolding,[],[f496,f478,f512]) ).
fof(f776,plain,
ron(vd1303,vd1297),
inference(definition_unfolding,[],[f502,f512]) ).
fof(f779,plain,
rR(sK4,sK6,vd1303),
inference(definition_unfolding,[],[f511,f482,f478,f512]) ).
fof(f780,plain,
rR(sK5,sK6,vd1300),
inference(definition_unfolding,[],[f509,f480,f478,f546]) ).
fof(f787,plain,
sK4 != sK6,
inference(definition_unfolding,[],[f534,f478,f482]) ).
fof(f788,plain,
sK5 != sK6,
inference(definition_unfolding,[],[f535,f478,f480]) ).
fof(f789,plain,
ron(sK4,vd1297),
inference(definition_unfolding,[],[f536,f482]) ).
fof(f790,plain,
ron(sK5,vd1295),
inference(definition_unfolding,[],[f537,f480]) ).
fof(f791,plain,
ron(sK6,vd1297),
inference(definition_unfolding,[],[f539,f478]) ).
fof(f792,plain,
ron(vd1300,vd1295),
inference(definition_unfolding,[],[f540,f546]) ).
fof(f793,plain,
ron(sK6,vd1295),
inference(definition_unfolding,[],[f541,f478]) ).
fof(f794,plain,
vd1300 != sK6,
inference(definition_unfolding,[],[f542,f478,f546]) ).
fof(f797,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = vd684
| X0 != X1
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(definition_unfolding,[],[f551,f584]) ).
fof(f798,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| vf(X0,X1) != vd684
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(definition_unfolding,[],[f550,f584]) ).
fof(f893,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X5,X12,X13] :
( vangle(X1,X0,X2) = vangle(X3,X0,X4)
| rR(X0,X2,X4)
| rR(X0,X1,X3)
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| ~ ron(X4,X7)
| ~ ron(X2,X7)
| ~ ron(X3,X5)
| ~ ron(X1,X5)
| ~ ron(X0,X5)
| ~ rline(X7)
| X5 != X8
| ~ rline(X8)
| X4 != X9
| ~ rpoint(X9)
| X3 != X10
| ~ rpoint(X10)
| X2 != X11
| ~ rpoint(X11)
| X1 != X12
| ~ rpoint(X12)
| X0 != X13
| ~ rpoint(X13) ),
inference(equality_resolution,[],[f487]) ).
fof(f894,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X12,X13] :
( vangle(X1,X0,X2) = vangle(X3,X0,X4)
| rR(X0,X2,X4)
| rR(X0,X1,X3)
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| ~ ron(X4,X7)
| ~ ron(X2,X7)
| ~ ron(X3,X8)
| ~ ron(X1,X8)
| ~ ron(X0,X8)
| ~ rline(X7)
| ~ rline(X8)
| X4 != X9
| ~ rpoint(X9)
| X3 != X10
| ~ rpoint(X10)
| X2 != X11
| ~ rpoint(X11)
| X1 != X12
| ~ rpoint(X12)
| X0 != X13
| ~ rpoint(X13) ),
inference(equality_resolution,[],[f893]) ).
fof(f895,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X12,X13] :
( vangle(X1,X0,X2) = vangle(X3,X0,X9)
| rR(X0,X2,X9)
| rR(X0,X1,X3)
| X0 = X9
| X0 = X3
| X0 = X2
| X0 = X1
| ~ ron(X9,X7)
| ~ ron(X2,X7)
| ~ ron(X3,X8)
| ~ ron(X1,X8)
| ~ ron(X0,X8)
| ~ rline(X7)
| ~ rline(X8)
| ~ rpoint(X9)
| X3 != X10
| ~ rpoint(X10)
| X2 != X11
| ~ rpoint(X11)
| X1 != X12
| ~ rpoint(X12)
| X0 != X13
| ~ rpoint(X13) ),
inference(equality_resolution,[],[f894]) ).
fof(f896,plain,
! [X2,X10,X0,X11,X1,X8,X9,X7,X12,X13] :
( vangle(X1,X0,X2) = vangle(X10,X0,X9)
| rR(X0,X2,X9)
| rR(X0,X1,X10)
| X0 = X9
| X0 = X10
| X0 = X2
| X0 = X1
| ~ ron(X9,X7)
| ~ ron(X2,X7)
| ~ ron(X10,X8)
| ~ ron(X1,X8)
| ~ ron(X0,X8)
| ~ rline(X7)
| ~ rline(X8)
| ~ rpoint(X9)
| ~ rpoint(X10)
| X2 != X11
| ~ rpoint(X11)
| X1 != X12
| ~ rpoint(X12)
| X0 != X13
| ~ rpoint(X13) ),
inference(equality_resolution,[],[f895]) ).
fof(f897,plain,
! [X10,X0,X11,X1,X8,X9,X7,X12,X13] :
( vangle(X10,X0,X9) = vangle(X1,X0,X11)
| rR(X0,X11,X9)
| rR(X0,X1,X10)
| X0 = X9
| X0 = X10
| X0 = X11
| X0 = X1
| ~ ron(X9,X7)
| ~ ron(X11,X7)
| ~ ron(X10,X8)
| ~ ron(X1,X8)
| ~ ron(X0,X8)
| ~ rline(X7)
| ~ rline(X8)
| ~ rpoint(X9)
| ~ rpoint(X10)
| ~ rpoint(X11)
| X1 != X12
| ~ rpoint(X12)
| X0 != X13
| ~ rpoint(X13) ),
inference(equality_resolution,[],[f896]) ).
fof(f898,plain,
! [X10,X0,X11,X8,X9,X7,X12,X13] :
( vangle(X10,X0,X9) = vangle(X12,X0,X11)
| rR(X0,X11,X9)
| rR(X0,X12,X10)
| X0 = X9
| X0 = X10
| X0 = X11
| X0 = X12
| ~ ron(X9,X7)
| ~ ron(X11,X7)
| ~ ron(X10,X8)
| ~ ron(X12,X8)
| ~ ron(X0,X8)
| ~ rline(X7)
| ~ rline(X8)
| ~ rpoint(X9)
| ~ rpoint(X10)
| ~ rpoint(X11)
| ~ rpoint(X12)
| X0 != X13
| ~ rpoint(X13) ),
inference(equality_resolution,[],[f897]) ).
fof(f899,plain,
! [X10,X11,X8,X9,X7,X12,X13] :
( ~ ron(X13,X8)
| rR(X13,X11,X9)
| rR(X13,X12,X10)
| X9 = X13
| X10 = X13
| X11 = X13
| X12 = X13
| ~ ron(X9,X7)
| ~ ron(X11,X7)
| ~ ron(X10,X8)
| ~ ron(X12,X8)
| vangle(X10,X13,X9) = vangle(X12,X13,X11)
| ~ rline(X7)
| ~ rline(X8)
| ~ rpoint(X9)
| ~ rpoint(X10)
| ~ rpoint(X11)
| ~ rpoint(X12)
| ~ rpoint(X13) ),
inference(equality_resolution,[],[f898]) ).
fof(f902,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( ~ rR(X0,X2,X4)
| vangle(X2,X0,X4) != vd684
| ~ ron(X2,X7)
| ~ ron(X0,X7)
| X0 = X4
| X0 = X2
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f768]) ).
fof(f903,plain,
! [X2,X3,X0,X1,X7,X5] :
( ~ rR(X0,X2,X5)
| vd684 != vangle(X2,X0,X5)
| ~ ron(X2,X7)
| ~ ron(X0,X7)
| X0 = X5
| X0 = X2
| ~ rline(X7)
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f902]) ).
fof(f904,plain,
! [X3,X0,X1,X7,X5] :
( ~ rR(X0,X3,X5)
| vd684 != vangle(X3,X0,X5)
| ~ ron(X3,X7)
| ~ ron(X0,X7)
| X0 = X5
| X0 = X3
| ~ rline(X7)
| ~ rpoint(X5)
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f903]) ).
fof(f905,plain,
! [X3,X1,X7,X5] :
( vd684 != vangle(X3,X1,X5)
| ~ rR(X1,X3,X5)
| ~ ron(X3,X7)
| ~ ron(X1,X7)
| X1 = X5
| X1 = X3
| ~ rline(X7)
| ~ rpoint(X5)
| ~ rpoint(X3)
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f904]) ).
fof(f906,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( ron(X4,X7)
| vangle(X2,X0,X4) != vd684
| ~ ron(X2,X7)
| ~ ron(X0,X7)
| X0 = X4
| X0 = X2
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f769]) ).
fof(f907,plain,
! [X2,X3,X0,X1,X7,X5] :
( ron(X5,X7)
| vd684 != vangle(X2,X0,X5)
| ~ ron(X2,X7)
| ~ ron(X0,X7)
| X0 = X5
| X0 = X2
| ~ rline(X7)
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f906]) ).
fof(f908,plain,
! [X3,X0,X1,X7,X5] :
( ron(X5,X7)
| vd684 != vangle(X3,X0,X5)
| ~ ron(X3,X7)
| ~ ron(X0,X7)
| X0 = X5
| X0 = X3
| ~ rline(X7)
| ~ rpoint(X5)
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f907]) ).
fof(f909,plain,
! [X3,X1,X7,X5] :
( vd684 != vangle(X3,X1,X5)
| ron(X5,X7)
| ~ ron(X3,X7)
| ~ ron(X1,X7)
| X1 = X5
| X1 = X3
| ~ rline(X7)
| ~ rpoint(X5)
| ~ rpoint(X3)
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f908]) ).
fof(f910,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( vangle(X2,X0,X4) = vd684
| rR(X0,X2,X4)
| ~ ron(X4,X7)
| ~ ron(X2,X7)
| ~ ron(X0,X7)
| X0 = X4
| X0 = X2
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f770]) ).
fof(f911,plain,
! [X2,X3,X0,X1,X7,X5] :
( vd684 = vangle(X2,X0,X5)
| rR(X0,X2,X5)
| ~ ron(X5,X7)
| ~ ron(X2,X7)
| ~ ron(X0,X7)
| X0 = X5
| X0 = X2
| ~ rline(X7)
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f910]) ).
fof(f912,plain,
! [X3,X0,X1,X7,X5] :
( vd684 = vangle(X3,X0,X5)
| rR(X0,X3,X5)
| ~ ron(X5,X7)
| ~ ron(X3,X7)
| ~ ron(X0,X7)
| X0 = X5
| X0 = X3
| ~ rline(X7)
| ~ rpoint(X5)
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f911]) ).
fof(f913,plain,
! [X3,X1,X7,X5] :
( ~ ron(X5,X7)
| rR(X1,X3,X5)
| vd684 = vangle(X3,X1,X5)
| ~ ron(X3,X7)
| ~ ron(X1,X7)
| X1 = X5
| X1 = X3
| ~ rline(X7)
| ~ rpoint(X5)
| ~ rpoint(X3)
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f912]) ).
fof(f952,plain,
! [X3,X0,X1,X4,X5] :
( vangle(X0,X1,X3) = vangle(X3,X1,X0)
| X0 = X3
| X0 = X1
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f524]) ).
fof(f953,plain,
! [X3,X0,X4,X5] :
( vangle(X0,X4,X3) = vangle(X3,X4,X0)
| X0 = X3
| X0 = X4
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f952]) ).
fof(f954,plain,
! [X3,X4,X5] :
( ~ rpoint(X5)
| X3 = X5
| X4 = X5
| ~ rpoint(X3)
| ~ rpoint(X4)
| vangle(X3,X4,X5) = vangle(X5,X4,X3) ),
inference(equality_resolution,[],[f953]) ).
fof(f958,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( rR(X1,X0,X4)
| ~ rR(X2,X1,X4)
| ~ rR(X1,X0,X2)
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f526]) ).
fof(f959,plain,
! [X0,X1,X6,X7,X4,X5] :
( rR(X1,X0,X4)
| ~ rR(X5,X1,X4)
| ~ rR(X1,X0,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f958]) ).
fof(f960,plain,
! [X0,X6,X7,X4,X5] :
( rR(X6,X0,X4)
| ~ rR(X5,X6,X4)
| ~ rR(X6,X0,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f959]) ).
fof(f961,plain,
! [X6,X7,X4,X5] :
( ~ rR(X6,X7,X5)
| ~ rR(X5,X6,X4)
| rR(X6,X7,X4)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f960]) ).
fof(f966,plain,
! [X3,X0,X1,X4,X5] :
( ~ rR(X0,X1,X3)
| ~ rR(X1,X0,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f531]) ).
fof(f967,plain,
! [X3,X0,X4,X5] :
( ~ rR(X0,X4,X3)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f966]) ).
fof(f968,plain,
! [X3,X4,X5] :
( ~ rR(X5,X4,X3)
| ~ rR(X4,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f967]) ).
fof(f969,plain,
! [X2,X3,X1,X4,X5] :
( ~ rR(X1,X2,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f530]) ).
fof(f970,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X3,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f969]) ).
fof(f971,plain,
! [X3,X4,X5] :
( ~ rR(X4,X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f970]) ).
fof(f972,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f971]) ).
fof(f973,plain,
! [X2,X3,X1,X4,X5] :
( ~ rR(X1,X1,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X1 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f529]) ).
fof(f974,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X1,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X1 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f973]) ).
fof(f975,plain,
! [X3,X4,X5] :
( ~ rR(X4,X4,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X4 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f974]) ).
fof(f976,plain,
! [X3,X5] :
( ~ rR(X5,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f975]) ).
fof(f977,plain,
! [X3,X0,X1,X4,X5] :
( rR(X1,X3,X0)
| ~ rR(X1,X0,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f528]) ).
fof(f978,plain,
! [X3,X0,X4,X5] :
( rR(X4,X3,X0)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f977]) ).
fof(f979,plain,
! [X3,X4,X5] :
( ~ rR(X4,X5,X3)
| rR(X4,X3,X5)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f978]) ).
fof(f984,plain,
! [X2,X3,X1] :
( vd684 = vf(X1,X1)
| X1 != X2
| ~ rpoint(X2)
| X1 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f797]) ).
fof(f985,plain,
! [X2,X3] :
( vd684 = vf(X2,X2)
| ~ rpoint(X2)
| X2 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f984]) ).
fof(f986,plain,
! [X3] :
( vd684 = vf(X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f985]) ).
fof(f987,plain,
! [X2,X3,X0] :
( X0 = X2
| vf(X0,X2) != vd684
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f798]) ).
fof(f988,plain,
! [X2,X3] :
( vd684 != vf(X3,X2)
| X2 = X3
| ~ rpoint(X2)
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f987]) ).
fof(f989,plain,
! [X3,X0,X4] :
( ron(X3,sK7(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f554]) ).
fof(f990,plain,
! [X3,X4] :
( ron(X3,sK7(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f989]) ).
fof(f991,plain,
! [X3,X0,X4] :
( ron(X0,sK7(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f553]) ).
fof(f992,plain,
! [X3,X4] :
( ron(X4,sK7(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f991]) ).
fof(f993,plain,
! [X3,X0,X4] :
( rline(sK7(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f552]) ).
fof(f994,plain,
! [X3,X4] :
( rline(sK7(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f993]) ).
fof(f1055,plain,
! [X2,X3,X0,X6,X4,X5] :
( X3 = X4
| vf(X2,X0) != vf(X2,X5)
| ~ ron(X5,X4)
| ~ ron(X0,X3)
| ~ rcenter(X2,X4)
| ~ rcenter(X2,X3)
| ~ rpoint(X5)
| X0 != X6
| ~ rpoint(X6) ),
inference(equality_resolution,[],[f580]) ).
fof(f1056,plain,
! [X2,X3,X6,X4,X5] :
( vf(X2,X5) != vf(X2,X6)
| X3 = X4
| ~ ron(X5,X4)
| ~ ron(X6,X3)
| ~ rcenter(X2,X4)
| ~ rcenter(X2,X3)
| ~ rpoint(X5)
| ~ rpoint(X6) ),
inference(equality_resolution,[],[f1055]) ).
fof(f1105,plain,
! [X3,X0,X4] :
( ron(X3,sK15(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f603]) ).
fof(f1106,plain,
! [X3,X4] :
( ron(X3,sK15(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1105]) ).
fof(f1107,plain,
! [X3,X0,X4] :
( rcenter(X0,sK15(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f602]) ).
fof(f1108,plain,
! [X3,X4] :
( rcenter(X4,sK15(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1107]) ).
fof(f1109,plain,
! [X3,X0,X4] :
( rcircle(sK15(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f601]) ).
fof(f1110,plain,
! [X3,X4] :
( rcircle(sK15(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1109]) ).
fof(f1200,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4] :
( rR(X0,X1,X2)
| X1 = X2
| ~ ron(X2,X6)
| ~ ron(X1,X6)
| ~ rinside(X0,X6)
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rcircle(X6)
| X3 != X4
| ~ rline(X4)
| X2 != X7
| ~ rpoint(X7)
| X1 != X8
| ~ rpoint(X8)
| X0 != X9
| ~ rpoint(X9) ),
inference(equality_resolution,[],[f631]) ).
fof(f1201,plain,
! [X2,X0,X1,X8,X6,X9,X7,X4] :
( rR(X0,X1,X2)
| X1 = X2
| ~ ron(X2,X6)
| ~ ron(X1,X6)
| ~ rinside(X0,X6)
| ~ ron(X2,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rcircle(X6)
| ~ rline(X4)
| X2 != X7
| ~ rpoint(X7)
| X1 != X8
| ~ rpoint(X8)
| X0 != X9
| ~ rpoint(X9) ),
inference(equality_resolution,[],[f1200]) ).
fof(f1202,plain,
! [X0,X1,X8,X6,X9,X7,X4] :
( rR(X0,X1,X7)
| X1 = X7
| ~ ron(X7,X6)
| ~ ron(X1,X6)
| ~ rinside(X0,X6)
| ~ ron(X7,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rcircle(X6)
| ~ rline(X4)
| ~ rpoint(X7)
| X1 != X8
| ~ rpoint(X8)
| X0 != X9
| ~ rpoint(X9) ),
inference(equality_resolution,[],[f1201]) ).
fof(f1203,plain,
! [X0,X8,X6,X9,X7,X4] :
( rR(X0,X8,X7)
| X7 = X8
| ~ ron(X7,X6)
| ~ ron(X8,X6)
| ~ rinside(X0,X6)
| ~ ron(X7,X4)
| ~ ron(X8,X4)
| ~ ron(X0,X4)
| ~ rcircle(X6)
| ~ rline(X4)
| ~ rpoint(X7)
| ~ rpoint(X8)
| X0 != X9
| ~ rpoint(X9) ),
inference(equality_resolution,[],[f1202]) ).
fof(f1204,plain,
! [X8,X6,X9,X7,X4] :
( ~ rinside(X9,X6)
| X7 = X8
| ~ ron(X7,X6)
| ~ ron(X8,X6)
| rR(X9,X8,X7)
| ~ ron(X7,X4)
| ~ ron(X8,X4)
| ~ ron(X9,X4)
| ~ rcircle(X6)
| ~ rline(X4)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9) ),
inference(equality_resolution,[],[f1203]) ).
fof(f1249,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ~ rR(X1,X2,X4)
| ~ rR(X1,X0,X4)
| ~ rR(X1,X0,X2)
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f641]) ).
fof(f1250,plain,
! [X0,X1,X6,X7,X4,X5] :
( ~ rR(X1,X5,X4)
| ~ rR(X1,X0,X4)
| ~ rR(X1,X0,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1249]) ).
fof(f1251,plain,
! [X0,X6,X7,X4,X5] :
( ~ rR(X6,X5,X4)
| ~ rR(X6,X0,X4)
| ~ rR(X6,X0,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1250]) ).
fof(f1252,plain,
! [X6,X7,X4,X5] :
( ~ rR(X6,X7,X5)
| ~ rR(X6,X7,X4)
| ~ rR(X6,X5,X4)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1251]) ).
fof(f1253,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( rR(X4,X0,X2)
| ~ rR(X4,X0,X1)
| ~ rR(X1,X0,X2)
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f642]) ).
fof(f1254,plain,
! [X0,X1,X6,X7,X4,X5] :
( rR(X4,X0,X5)
| ~ rR(X4,X0,X1)
| ~ rR(X1,X0,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1253]) ).
fof(f1255,plain,
! [X0,X6,X7,X4,X5] :
( rR(X4,X0,X5)
| ~ rR(X4,X0,X6)
| ~ rR(X6,X0,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1254]) ).
fof(f1256,plain,
! [X6,X7,X4,X5] :
( ~ rR(X6,X7,X5)
| ~ rR(X4,X7,X6)
| rR(X4,X7,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1255]) ).
fof(f1573,definition,
sF52 = vangle(sK6,sK4,sK5),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f1574,plain,
vangle(sK6,sK4,sK5) = sF52,
inference(reorient_equations,[],[f1573]) ).
fof(f1575,definition,
sF53 = vangle(sK6,sK5,sK4),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f1576,plain,
vangle(sK6,sK5,sK4) = sF53,
inference(reorient_equations,[],[f1575]) ).
fof(f1577,plain,
sF52 != sF53,
inference(definition_folding,[],[f753,f1576,f1574]) ).
fof(f1578,plain,
! [X3] :
( ~ rpoint(X3)
| vd684 = vf(X3,X3) ),
inference(duplicate_literal_removal,[],[f986]) ).
fof(f1579,plain,
! [X3,X5] :
( ~ rR(X5,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X5) ),
inference(duplicate_literal_removal,[],[f976]) ).
fof(f1580,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f972]) ).
fof(f1630,plain,
( rR(sK5,vd1300,sK6)
| ~ rpoint(vd1300)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(resolution,[],[f979,f780]) ).
fof(f1631,plain,
( rR(sK4,vd1303,sK6)
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(resolution,[],[f979,f779]) ).
fof(f1632,plain,
( rR(sK4,vd1303,sK6)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1631,f510]) ).
fof(f1633,plain,
( rR(sK5,vd1300,sK6)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1630,f547]) ).
fof(f1634,plain,
( rR(sK4,vd1303,sK6)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1632,f481]) ).
fof(f1635,plain,
( rR(sK5,vd1300,sK6)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1633,f479]) ).
fof(f1636,plain,
rR(sK4,vd1303,sK6),
inference(forward_subsumption_resolution,[],[f1634,f477]) ).
fof(f1637,plain,
rR(sK5,vd1300,sK6),
inference(forward_subsumption_resolution,[],[f1635,f477]) ).
fof(f1639,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK6,X0,X1)
| rR(sK6,X2,X3)
| sK6 = X1
| sK6 = X3
| sK6 = X0
| sK6 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1295)
| ~ ron(X2,vd1295)
| vangle(X3,sK6,X1) = vangle(X2,sK6,X0)
| ~ rline(X4)
| ~ rline(vd1295)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK6) ),
inference(resolution,[],[f899,f793]) ).
fof(f1640,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK4,X0,X1)
| rR(sK4,X2,X3)
| sK4 = X1
| sK4 = X3
| sK4 = X0
| sK4 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK4,X1) = vangle(X2,sK4,X0)
| ~ rline(X4)
| ~ rline(vd1297)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK4) ),
inference(resolution,[],[f899,f789]) ).
fof(f1642,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK6,X0,X1)
| rR(sK6,X2,X3)
| sK6 = X1
| sK6 = X3
| sK6 = X0
| sK6 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK6,X1) = vangle(X2,sK6,X0)
| ~ rline(X4)
| ~ rline(vd1297)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK6) ),
inference(resolution,[],[f791,f899]) ).
fof(f1659,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK4 = X1
| ~ rpoint(X0)
| sK4 = X0
| vangle(X0,X1,sK4) = vangle(sK4,X1,X0) ),
inference(resolution,[],[f954,f481]) ).
fof(f1660,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK5 = X1
| ~ rpoint(X0)
| sK5 = X0
| vangle(X0,X1,sK5) = vangle(sK5,X1,X0) ),
inference(resolution,[],[f954,f479]) ).
fof(f1666,plain,
vd684 = vf(sK4,sK4),
inference(resolution,[],[f1578,f481]) ).
fof(f1670,plain,
( ~ rR(sK6,sK4,vd1303)
| ~ rpoint(vd1303)
| ~ rpoint(sK6)
| ~ rpoint(sK4) ),
inference(resolution,[],[f968,f779]) ).
fof(f1672,plain,
( ~ rR(vd1300,sK5,sK6)
| ~ rpoint(sK6)
| ~ rpoint(vd1300)
| ~ rpoint(sK5) ),
inference(resolution,[],[f968,f1637]) ).
fof(f1677,plain,
( ~ rR(vd1300,sK5,sK6)
| ~ rpoint(vd1300)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f1672,f477]) ).
fof(f1679,plain,
( ~ rR(sK6,sK4,vd1303)
| ~ rpoint(sK6)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f1670,f510]) ).
fof(f1682,plain,
( ~ rR(vd1300,sK5,sK6)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f1677,f547]) ).
fof(f1684,plain,
( ~ rR(sK6,sK4,vd1303)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f1679,f477]) ).
fof(f1687,plain,
~ rR(vd1300,sK5,sK6),
inference(forward_subsumption_resolution,[],[f1682,f479]) ).
fof(f1689,plain,
~ rR(sK6,sK4,vd1303),
inference(forward_subsumption_resolution,[],[f1684,f481]) ).
fof(f1713,plain,
! [X0] :
( ~ rR(X0,sK6,sK5)
| rR(X0,sK6,vd1300)
| ~ rpoint(X0)
| ~ rpoint(vd1300)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(resolution,[],[f1256,f780]) ).
fof(f1716,plain,
! [X0] :
( ~ rR(X0,vd1300,sK5)
| rR(X0,vd1300,sK6)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(vd1300) ),
inference(resolution,[],[f1256,f1637]) ).
fof(f1717,plain,
! [X0] :
( ~ rR(X0,vd1303,sK4)
| rR(X0,vd1303,sK6)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) ),
inference(resolution,[],[f1256,f1636]) ).
fof(f1720,plain,
! [X0] :
( ~ rR(X0,vd1303,sK4)
| rR(X0,vd1303,sK6)
| ~ rpoint(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) ),
inference(forward_subsumption_resolution,[],[f1717,f477]) ).
fof(f1721,plain,
! [X0] :
( ~ rR(X0,vd1300,sK5)
| rR(X0,vd1300,sK6)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f1716,f477]) ).
fof(f1724,plain,
! [X0] :
( ~ rR(X0,sK6,sK5)
| rR(X0,sK6,vd1300)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1713,f547]) ).
fof(f1726,plain,
! [X0] :
( ~ rR(X0,vd1303,sK4)
| rR(X0,vd1303,sK6)
| ~ rpoint(X0)
| ~ rpoint(vd1303) ),
inference(forward_subsumption_resolution,[],[f1720,f481]) ).
fof(f1727,plain,
! [X0] :
( ~ rR(X0,vd1300,sK5)
| rR(X0,vd1300,sK6)
| ~ rpoint(X0)
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f1721,f479]) ).
fof(f1730,plain,
! [X0] :
( ~ rR(X0,sK6,sK5)
| rR(X0,sK6,vd1300)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1724,f479]) ).
fof(f1732,plain,
! [X0] :
( ~ rR(X0,vd1303,sK4)
| rR(X0,vd1303,sK6)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1726,f510]) ).
fof(f1733,plain,
! [X0] :
( ~ rR(X0,vd1300,sK5)
| rR(X0,vd1300,sK6)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1727,f547]) ).
fof(f1736,plain,
! [X0] :
( ~ rR(X0,sK6,sK5)
| rR(X0,sK6,vd1300)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1730,f477]) ).
fof(f1741,plain,
! [X0] :
( ~ rR(sK6,sK5,X0)
| rR(sK5,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(vd1300) ),
inference(resolution,[],[f961,f1637]) ).
fof(f1746,plain,
! [X0] :
( ~ rR(sK6,sK5,X0)
| rR(sK5,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f1741,f477]) ).
fof(f1752,plain,
! [X0] :
( ~ rR(sK6,sK5,X0)
| rR(sK5,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f1746,f479]) ).
fof(f1758,plain,
! [X0] :
( ~ rR(sK6,sK5,X0)
| rR(sK5,vd1300,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1752,f547]) ).
fof(f1766,definition,
( spl54_13
<=> vd1300 = sK4 ),
introduced(definition,[new_symbols(definition,[spl54_13])],[avatar_definition]) ).
fof(f1767,plain,
( vd1300 != sK4
| spl54_13 ),
inference(avatar_component_clause,[],[f1766]) ).
fof(f1768,plain,
( vd1300 = sK4
| ~ spl54_13 ),
inference(avatar_component_clause,[],[f1766]) ).
fof(f1770,definition,
( spl54_14
<=> vd684 = vf(sK5,vd1306) ),
introduced(definition,[new_symbols(definition,[spl54_14])],[avatar_definition]) ).
fof(f1771,plain,
( vd684 = vf(sK5,vd1306)
| ~ spl54_14 ),
inference(avatar_component_clause,[],[f1770]) ).
fof(f1772,plain,
( vd684 != vf(sK5,vd1306)
| spl54_14 ),
inference(avatar_component_clause,[],[f1770]) ).
fof(f1783,definition,
( spl54_15
<=> vd1300 = sK5 ),
introduced(definition,[new_symbols(definition,[spl54_15])],[avatar_definition]) ).
fof(f1784,plain,
( vd1300 != sK5
| spl54_15 ),
inference(avatar_component_clause,[],[f1783]) ).
fof(f1785,plain,
( vd1300 = sK5
| ~ spl54_15 ),
inference(avatar_component_clause,[],[f1783]) ).
fof(f1798,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X0)
| vd684 = vangle(X3,X2,X0)
| ~ ron(X3,sK7(X1,X0))
| ~ ron(X2,sK7(X1,X0))
| X0 = X2
| X2 = X3
| ~ rline(sK7(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(resolution,[],[f990,f913]) ).
fof(f1801,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X0)
| vd684 = vangle(X3,X2,X0)
| ~ ron(X3,sK7(X1,X0))
| ~ ron(X2,sK7(X1,X0))
| X0 = X2
| X2 = X3
| ~ rline(sK7(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f1798]) ).
fof(f1804,plain,
! [X2,X3,X0,X1] :
( ~ ron(X3,sK7(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X0)
| vd684 = vangle(X3,X2,X0)
| X0 = X1
| ~ ron(X2,sK7(X1,X0))
| X0 = X2
| X2 = X3
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f1801,f994]) ).
fof(f1806,plain,
! [X2,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X0,X0)
| vd684 = vangle(X0,X2,X0)
| X0 = X1
| ~ ron(X2,sK7(X1,X0))
| X0 = X2
| X0 = X2
| ~ rpoint(X0)
| ~ rpoint(X2)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f1804,f990]) ).
fof(f1807,plain,
! [X2,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X0,X0)
| vd684 = vangle(X0,X2,X0)
| X0 = X1
| ~ ron(X2,sK7(X1,X0))
| X0 = X2
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f1806]) ).
fof(f1808,plain,
! [X2,X0,X1] :
( ~ ron(X2,sK7(X1,X0))
| ~ rpoint(X1)
| vd684 = vangle(X0,X2,X0)
| X0 = X1
| ~ rpoint(X0)
| X0 = X2
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f1807,f1580]) ).
fof(f1813,plain,
! [X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rpoint(X1)
| vd684 = vangle(X0,X1,X0)
| X0 = X1
| ~ rpoint(X0)
| X0 = X1
| ~ rpoint(X1) ),
inference(resolution,[],[f992,f1808]) ).
fof(f1817,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X1,X2,X3)
| rR(X1,X4,X5)
| X1 = X3
| X1 = X5
| X1 = X2
| X1 = X4
| ~ ron(X3,X6)
| ~ ron(X2,X6)
| ~ ron(X5,sK7(X1,X0))
| ~ ron(X4,sK7(X1,X0))
| vangle(X5,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X6)
| ~ rline(sK7(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1) ),
inference(resolution,[],[f992,f899]) ).
fof(f1818,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X1,X2,X3)
| rR(X1,X4,X5)
| X1 = X3
| X1 = X5
| X1 = X2
| X1 = X4
| ~ ron(X3,X6)
| ~ ron(X2,X6)
| ~ ron(X5,sK7(X1,X0))
| ~ ron(X4,sK7(X1,X0))
| vangle(X5,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X6)
| ~ rline(sK7(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f1817]) ).
fof(f1822,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X1
| vd684 = vangle(X0,X1,X0) ),
inference(duplicate_literal_removal,[],[f1813]) ).
fof(f1823,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ ron(X5,sK7(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X1,X2,X3)
| rR(X1,X4,X5)
| X1 = X3
| X1 = X5
| X1 = X2
| X1 = X4
| ~ ron(X3,X6)
| ~ ron(X2,X6)
| X0 = X1
| ~ ron(X4,sK7(X1,X0))
| vangle(X5,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X6)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(forward_subsumption_resolution,[],[f1818,f994]) ).
fof(f1829,plain,
! [X0] :
( ~ rpoint(X0)
| sK4 = X0
| vd684 = vangle(X0,sK4,X0) ),
inference(resolution,[],[f1822,f481]) ).
fof(f1830,plain,
! [X0] :
( ~ rpoint(X0)
| sK5 = X0
| vd684 = vangle(X0,sK5,X0) ),
inference(resolution,[],[f1822,f479]) ).
fof(f1831,plain,
! [X0] :
( ~ rpoint(X0)
| sK6 = X0
| vd684 = vangle(X0,sK6,X0) ),
inference(resolution,[],[f1822,f477]) ).
fof(f1848,plain,
( sK5 = sK6
| vd684 = vangle(sK5,sK6,sK5) ),
inference(resolution,[],[f1831,f479]) ).
fof(f1850,plain,
vd684 = vangle(sK5,sK6,sK5),
inference(forward_subsumption_resolution,[],[f1848,f788]) ).
fof(f1858,definition,
( spl54_18
<=> vd1303 = sK6 ),
introduced(definition,[new_symbols(definition,[spl54_18])],[avatar_definition]) ).
fof(f1859,plain,
( vd1303 != sK6
| spl54_18 ),
inference(avatar_component_clause,[],[f1858]) ).
fof(f1860,plain,
( vd1303 = sK6
| ~ spl54_18 ),
inference(avatar_component_clause,[],[f1858]) ).
fof(f1878,plain,
( sK4 = sK6
| vd684 = vangle(sK6,sK4,sK6) ),
inference(resolution,[],[f1829,f477]) ).
fof(f1879,plain,
vd684 = vangle(sK6,sK4,sK6),
inference(forward_subsumption_resolution,[],[f1878,f787]) ).
fof(f1908,plain,
( vf(sK5,vd1306) = vf(sK4,sK4)
| ~ spl54_13 ),
inference(superposition,[],[f759,f1768]) ).
fof(f1918,plain,
( vd684 = vf(sK5,vd1306)
| ~ spl54_13 ),
inference(forward_demodulation,[],[f1908,f1666]) ).
fof(f1920,plain,
( $false
| ~ spl54_13
| spl54_14 ),
inference(forward_subsumption_resolution,[],[f1918,f1772]) ).
fof(f1921,plain,
( ~ spl54_13
| spl54_14 ),
inference(avatar_contradiction_clause,[],[f1920]) ).
fof(f1922,plain,
( vd684 != vd684
| vd1306 = sK5
| ~ rpoint(vd1306)
| ~ rpoint(sK5)
| ~ spl54_14 ),
inference(superposition,[],[f988,f1771]) ).
fof(f1923,plain,
( vd1306 = sK5
| ~ rpoint(vd1306)
| ~ rpoint(sK5)
| ~ spl54_14 ),
inference(trivial_inequality_removal,[],[f1922]) ).
fof(f1924,plain,
( vd1306 = sK5
| ~ rpoint(sK5)
| ~ spl54_14 ),
inference(forward_subsumption_resolution,[],[f1923,f476]) ).
fof(f1925,plain,
( vd1306 = sK5
| ~ spl54_14 ),
inference(forward_subsumption_resolution,[],[f1924,f479]) ).
fof(f1933,plain,
( rR(sK5,sK6,vd1303)
| ~ spl54_14 ),
inference(superposition,[],[f773,f1925]) ).
fof(f2016,plain,
( sK5 = sK6
| vd684 = vangle(sK6,sK5,sK6) ),
inference(resolution,[],[f1830,f477]) ).
fof(f2017,plain,
vd684 = vangle(sK6,sK5,sK6),
inference(forward_subsumption_resolution,[],[f2016,f788]) ).
fof(f2024,definition,
( spl54_25
<=> vd1303 = sK5 ),
introduced(definition,[new_symbols(definition,[spl54_25])],[avatar_definition]) ).
fof(f2025,plain,
( vd1303 != sK5
| spl54_25 ),
inference(avatar_component_clause,[],[f2024]) ).
fof(f2026,plain,
( vd1303 = sK5
| ~ spl54_25 ),
inference(avatar_component_clause,[],[f2024]) ).
fof(f2103,plain,
! [X0] :
( ~ rR(sK5,sK6,X0)
| ~ rR(sK5,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1300)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(resolution,[],[f1252,f780]) ).
fof(f2106,plain,
! [X0] :
( ~ rR(sK4,sK6,X0)
| ~ rR(sK4,vd1303,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(resolution,[],[f1252,f779]) ).
fof(f2109,plain,
! [X0] :
( ~ rR(sK4,sK6,X0)
| ~ rR(sK4,vd1303,X0)
| ~ rpoint(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f2106,f510]) ).
fof(f2112,plain,
! [X0] :
( ~ rR(sK5,sK6,X0)
| ~ rR(sK5,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f2103,f547]) ).
fof(f2119,plain,
! [X0] :
( ~ rR(sK4,sK6,X0)
| ~ rR(sK4,vd1303,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f2109,f481]) ).
fof(f2122,plain,
! [X0] :
( ~ rR(sK5,sK6,X0)
| ~ rR(sK5,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f2112,f479]) ).
fof(f2129,plain,
! [X0] :
( ~ rR(sK4,sK6,X0)
| ~ rR(sK4,vd1303,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2119,f477]) ).
fof(f2132,plain,
! [X0] :
( ~ rR(sK5,sK6,X0)
| ~ rR(sK5,vd1300,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2122,f477]) ).
fof(f2144,plain,
( ~ rR(sK4,vd1303,vd1303)
| ~ rpoint(vd1303) ),
inference(resolution,[],[f2129,f779]) ).
fof(f2145,plain,
~ rR(sK4,vd1303,vd1303),
inference(forward_subsumption_resolution,[],[f2144,f510]) ).
fof(f2179,plain,
! [X0] :
( sK4 = sK6
| ~ rpoint(X0)
| sK4 = X0
| vangle(X0,sK6,sK4) = vangle(sK4,sK6,X0) ),
inference(resolution,[],[f1659,f477]) ).
fof(f2180,plain,
! [X0] :
( ~ rpoint(X0)
| sK4 = X0
| vangle(X0,sK6,sK4) = vangle(sK4,sK6,X0) ),
inference(forward_subsumption_resolution,[],[f2179,f787]) ).
fof(f2245,plain,
( sK4 = sK5
| vangle(sK5,sK6,sK4) = vangle(sK4,sK6,sK5) ),
inference(resolution,[],[f2180,f479]) ).
fof(f2248,plain,
vangle(sK5,sK6,sK4) = vangle(sK4,sK6,sK5),
inference(forward_subsumption_resolution,[],[f2245,f763]) ).
fof(f2264,plain,
! [X0] :
( sK5 = sK6
| ~ rpoint(X0)
| sK5 = X0
| vangle(X0,sK6,sK5) = vangle(sK5,sK6,X0) ),
inference(resolution,[],[f1660,f477]) ).
fof(f2265,plain,
! [X0] :
( ~ rpoint(X0)
| sK5 = X0
| vangle(X0,sK6,sK5) = vangle(sK5,sK6,X0) ),
inference(forward_subsumption_resolution,[],[f2264,f788]) ).
fof(f2376,plain,
( rR(sK5,sK5,sK6)
| ~ spl54_15 ),
inference(superposition,[],[f1637,f1785]) ).
fof(f2377,plain,
( ~ rR(sK5,sK5,sK6)
| ~ spl54_15 ),
inference(superposition,[],[f1687,f1785]) ).
fof(f2381,plain,
( $false
| ~ spl54_15 ),
inference(forward_subsumption_resolution,[],[f2376,f2377]) ).
fof(f2382,plain,
~ spl54_15,
inference(avatar_contradiction_clause,[],[f2381]) ).
fof(f2493,plain,
( vd1303 = sK5
| vangle(vd1303,sK6,sK5) = vangle(sK5,sK6,vd1303) ),
inference(resolution,[],[f2265,f510]) ).
fof(f2494,plain,
( vd1300 = sK5
| vangle(vd1300,sK6,sK5) = vangle(sK5,sK6,vd1300) ),
inference(resolution,[],[f2265,f547]) ).
fof(f2499,plain,
( vangle(vd1300,sK6,sK5) = vangle(sK5,sK6,vd1300)
| spl54_15 ),
inference(forward_subsumption_resolution,[],[f2494,f1784]) ).
fof(f2567,plain,
( rR(sK4,sK6,sK6)
| ~ spl54_18 ),
inference(superposition,[],[f779,f1860]) ).
fof(f2575,plain,
( ~ rR(sK4,sK6,sK6)
| ~ spl54_18 ),
inference(superposition,[],[f2145,f1860]) ).
fof(f2582,plain,
( $false
| ~ spl54_18 ),
inference(forward_subsumption_resolution,[],[f2567,f2575]) ).
fof(f2583,plain,
~ spl54_18,
inference(avatar_contradiction_clause,[],[f2582]) ).
fof(f2761,plain,
! [X0] :
( vd684 != vangle(sK4,sK6,sK5)
| ron(sK4,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| sK4 = sK6
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(superposition,[],[f909,f2248]) ).
fof(f2762,plain,
! [X0] :
( vd684 != vangle(sK4,sK6,sK5)
| ~ rR(sK6,sK5,sK4)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| sK4 = sK6
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(superposition,[],[f905,f2248]) ).
fof(f2870,plain,
! [X2,X0,X1] :
( vf(sK6,sK4) != vf(sK6,X0)
| X1 = X2
| ~ ron(X0,X2)
| ~ ron(sK5,X1)
| ~ rcenter(sK6,X2)
| ~ rcenter(sK6,X1)
| ~ rpoint(X0)
| ~ rpoint(sK5) ),
inference(superposition,[],[f1056,f762]) ).
fof(f2877,plain,
! [X2,X0,X1] :
( vf(sK6,sK4) != vf(sK6,X0)
| X1 = X2
| ~ ron(X0,X2)
| ~ ron(sK5,X1)
| ~ rcenter(sK6,X2)
| ~ rcenter(sK6,X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2870,f479]) ).
fof(f4224,plain,
! [X0,X1] :
( rinside(X0,sK15(X0,X1))
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f643,f1108]) ).
fof(f4225,plain,
! [X2,X3,X0,X1,X4] :
( X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0)
| X2 = X3
| ~ ron(X2,sK15(X0,X1))
| ~ ron(X3,sK15(X0,X1))
| rR(X0,X3,X2)
| ~ ron(X2,X4)
| ~ ron(X3,X4)
| ~ ron(X0,X4)
| ~ rcircle(sK15(X0,X1))
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X0) ),
inference(resolution,[],[f4224,f1204]) ).
fof(f4226,plain,
! [X2,X3,X0,X1,X4] :
( X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0)
| X2 = X3
| ~ ron(X2,sK15(X0,X1))
| ~ ron(X3,sK15(X0,X1))
| rR(X0,X3,X2)
| ~ ron(X2,X4)
| ~ ron(X3,X4)
| ~ ron(X0,X4)
| ~ rcircle(sK15(X0,X1))
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X3) ),
inference(duplicate_literal_removal,[],[f4225]) ).
fof(f4227,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,sK15(X0,X1))
| ~ rpoint(X1)
| ~ rpoint(X0)
| X2 = X3
| ~ ron(X2,sK15(X0,X1))
| X0 = X1
| rR(X0,X3,X2)
| ~ ron(X2,X4)
| ~ ron(X3,X4)
| ~ ron(X0,X4)
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X3) ),
inference(forward_subsumption_resolution,[],[f4226,f1110]) ).
fof(f7207,plain,
! [X0,X1] :
( X0 = X1
| ~ ron(sK4,X1)
| ~ ron(sK5,X0)
| ~ rcenter(sK6,X1)
| ~ rcenter(sK6,X0)
| ~ rpoint(sK4) ),
inference(equality_resolution,[],[f2877]) ).
fof(f7213,plain,
! [X0,X1] :
( ~ rcenter(sK6,X1)
| ~ ron(sK4,X1)
| ~ ron(sK5,X0)
| X0 = X1
| ~ rcenter(sK6,X0) ),
inference(forward_subsumption_resolution,[],[f7207,f481]) ).
fof(f7230,plain,
! [X0,X1] :
( ~ ron(sK4,sK15(sK6,X0))
| ~ ron(sK5,X1)
| sK15(sK6,X0) = X1
| ~ rcenter(sK6,X1)
| sK6 = X0
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(resolution,[],[f7213,f1108]) ).
fof(f7231,plain,
! [X0,X1] :
( ~ ron(sK4,sK15(sK6,X0))
| ~ ron(sK5,X1)
| sK15(sK6,X0) = X1
| ~ rcenter(sK6,X1)
| sK6 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f7230,f477]) ).
fof(f7250,plain,
! [X0] :
( ~ ron(sK5,X0)
| sK15(sK6,sK4) = X0
| ~ rcenter(sK6,X0)
| sK4 = sK6
| ~ rpoint(sK4)
| sK4 = sK6
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(resolution,[],[f7231,f1106]) ).
fof(f7251,plain,
! [X0] :
( ~ ron(sK5,X0)
| sK15(sK6,sK4) = X0
| ~ rcenter(sK6,X0)
| sK4 = sK6
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(duplicate_literal_removal,[],[f7250]) ).
fof(f7252,plain,
! [X0] :
( ~ ron(sK5,X0)
| sK15(sK6,sK4) = X0
| ~ rcenter(sK6,X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f7251,f787]) ).
fof(f7253,plain,
! [X0] :
( ~ ron(sK5,X0)
| sK15(sK6,sK4) = X0
| ~ rcenter(sK6,X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f7252,f481]) ).
fof(f7254,plain,
! [X0] :
( ~ rcenter(sK6,X0)
| sK15(sK6,sK4) = X0
| ~ ron(sK5,X0) ),
inference(forward_subsumption_resolution,[],[f7253,f477]) ).
fof(f7255,plain,
! [X0] :
( sK15(sK6,X0) = sK15(sK6,sK4)
| ~ ron(sK5,sK15(sK6,X0))
| sK6 = X0
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(resolution,[],[f7254,f1108]) ).
fof(f7256,plain,
! [X0] :
( ~ ron(sK5,sK15(sK6,X0))
| sK15(sK6,X0) = sK15(sK6,sK4)
| sK6 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f7255,f477]) ).
fof(f7257,plain,
( sK15(sK6,sK4) = sK15(sK6,sK5)
| sK5 = sK6
| ~ rpoint(sK5)
| sK5 = sK6
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(resolution,[],[f7256,f1106]) ).
fof(f7258,plain,
( sK15(sK6,sK4) = sK15(sK6,sK5)
| sK5 = sK6
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(duplicate_literal_removal,[],[f7257]) ).
fof(f7259,plain,
( sK15(sK6,sK4) = sK15(sK6,sK5)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f7258,f788]) ).
fof(f7260,plain,
( sK15(sK6,sK4) = sK15(sK6,sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f7259,f479]) ).
fof(f7261,plain,
sK15(sK6,sK4) = sK15(sK6,sK5),
inference(forward_subsumption_resolution,[],[f7260,f477]) ).
fof(f7266,plain,
( ron(sK5,sK15(sK6,sK4))
| sK5 = sK6
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(superposition,[],[f1106,f7261]) ).
fof(f7267,plain,
( ron(sK5,sK15(sK6,sK4))
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f7266,f788]) ).
fof(f7271,plain,
( ron(sK5,sK15(sK6,sK4))
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f7267,f479]) ).
fof(f7275,plain,
ron(sK5,sK15(sK6,sK4)),
inference(forward_subsumption_resolution,[],[f7271,f477]) ).
fof(f13805,plain,
( vangle(vd1303,sK6,sK5) = vangle(sK5,sK6,vd1303)
| spl54_25 ),
inference(forward_subsumption_resolution,[],[f2493,f2025]) ).
fof(f20341,definition,
( spl54_730
<=> vd684 = sF53 ),
introduced(definition,[new_symbols(definition,[spl54_730])],[avatar_definition]) ).
fof(f20342,plain,
( vd684 = sF53
| ~ spl54_730 ),
inference(avatar_component_clause,[],[f20341]) ).
fof(f20343,plain,
( vd684 != sF53
| spl54_730 ),
inference(avatar_component_clause,[],[f20341]) ).
fof(f20685,definition,
( spl54_732
<=> vd684 = sF52 ),
introduced(definition,[new_symbols(definition,[spl54_732])],[avatar_definition]) ).
fof(f20687,plain,
( vd684 != sF52
| spl54_732 ),
inference(avatar_component_clause,[],[f20685]) ).
fof(f21160,definition,
( spl54_738
<=> vd684 = vangle(sK4,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_738])],[avatar_definition]) ).
fof(f21162,plain,
( vd684 != vangle(sK4,sK6,sK5)
| spl54_738 ),
inference(avatar_component_clause,[],[f21160]) ).
fof(f21477,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK4,X0,X1)
| rR(sK4,X2,X3)
| sK4 = X1
| sK4 = X3
| sK4 = X0
| sK4 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK4,X1) = vangle(X2,sK4,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f1640,f515]) ).
fof(f21478,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK6,X0,X1)
| rR(sK6,X2,X3)
| sK6 = X1
| sK6 = X3
| sK6 = X0
| sK6 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1295)
| ~ ron(X2,vd1295)
| vangle(X3,sK6,X1) = vangle(X2,sK6,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1639,f518]) ).
fof(f21480,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK6,X0,X1)
| rR(sK6,X2,X3)
| sK6 = X1
| sK6 = X3
| sK6 = X0
| sK6 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK6,X1) = vangle(X2,sK6,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1642,f515]) ).
fof(f21533,plain,
! [X0] :
( vd684 != vangle(sK4,sK6,sK5)
| ron(sK4,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f2761,f787]) ).
fof(f21534,plain,
! [X0] :
( vd684 != vangle(sK4,sK6,sK5)
| ~ rR(sK6,sK5,sK4)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f2762,f787]) ).
fof(f22015,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,vd1297)
| rR(sK4,X2,X3)
| sK4 = X1
| sK4 = X3
| sK4 = X0
| sK4 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| rR(sK4,X0,X1)
| ~ ron(X2,vd1297)
| vangle(X3,sK4,X1) = vangle(X2,sK4,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f21477,f481]) ).
fof(f22016,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,vd1295)
| rR(sK6,X2,X3)
| sK6 = X1
| sK6 = X3
| sK6 = X0
| sK6 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| rR(sK6,X0,X1)
| ~ ron(X2,vd1295)
| vangle(X3,sK6,X1) = vangle(X2,sK6,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f21478,f477]) ).
fof(f22018,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,vd1297)
| rR(sK6,X2,X3)
| sK6 = X1
| sK6 = X3
| sK6 = X0
| sK6 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| rR(sK6,X0,X1)
| ~ ron(X2,vd1297)
| vangle(X3,sK6,X1) = vangle(X2,sK6,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f21480,f477]) ).
fof(f22069,plain,
! [X0] :
( vd684 != vangle(sK4,sK6,sK5)
| ron(sK4,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f21533,f788]) ).
fof(f22070,plain,
! [X0] :
( vd684 != vangle(sK4,sK6,sK5)
| ~ rR(sK6,sK5,sK4)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f21534,f788]) ).
fof(f22910,plain,
! [X0] :
( vd684 != vangle(sK4,sK6,sK5)
| ron(sK4,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f22069,f481]) ).
fof(f22911,plain,
! [X0] :
( vd684 != vangle(sK4,sK6,sK5)
| ~ rR(sK6,sK5,sK4)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f22070,f481]) ).
fof(f23550,plain,
! [X0] :
( vd684 != vangle(sK4,sK6,sK5)
| ron(sK4,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f22910,f479]) ).
fof(f23551,plain,
! [X0] :
( vd684 != vangle(sK4,sK6,sK5)
| ~ rR(sK6,sK5,sK4)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f22911,f479]) ).
fof(f23918,plain,
! [X0] :
( vd684 != vangle(sK4,sK6,sK5)
| ron(sK4,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f23550,f477]) ).
fof(f23919,plain,
! [X0] :
( vd684 != vangle(sK4,sK6,sK5)
| ~ rR(sK6,sK5,sK4)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f23551,f477]) ).
fof(f24253,definition,
( spl54_1009
<=> ! [X0] :
( ron(sK4,X0)
| ~ rline(X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_1009])],[avatar_definition]) ).
fof(f24254,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ rline(X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0) )
| ~ spl54_1009 ),
inference(avatar_component_clause,[],[f24253]) ).
fof(f24255,plain,
( spl54_1009
| ~ spl54_738 ),
inference(avatar_split_clause,[],[f23918,f21160,f24253]) ).
fof(f24257,definition,
( spl54_1010
<=> ! [X0] :
( ~ ron(sK5,X0)
| ~ rline(X0)
| ~ ron(sK6,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_1010])],[avatar_definition]) ).
fof(f24258,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(sK5,X0) )
| ~ spl54_1010 ),
inference(avatar_component_clause,[],[f24257]) ).
fof(f24260,definition,
( spl54_1011
<=> rR(sK6,sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl54_1011])],[avatar_definition]) ).
fof(f24261,plain,
( rR(sK6,sK5,sK4)
| ~ spl54_1011 ),
inference(avatar_component_clause,[],[f24260]) ).
fof(f24262,plain,
( ~ rR(sK6,sK5,sK4)
| spl54_1011 ),
inference(avatar_component_clause,[],[f24260]) ).
fof(f24263,plain,
( spl54_1010
| ~ spl54_1011
| ~ spl54_738 ),
inference(avatar_split_clause,[],[f23919,f21160,f24260,f24257]) ).
fof(f24846,definition,
( spl54_1075
<=> rR(sK5,vd1300,sK4) ),
introduced(definition,[new_symbols(definition,[spl54_1075])],[avatar_definition]) ).
fof(f24848,plain,
( ~ rR(sK5,vd1300,sK4)
| spl54_1075 ),
inference(avatar_component_clause,[],[f24846]) ).
fof(f24925,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X1,X2,X3)
| rR(X1,X4,X0)
| X1 = X3
| X0 = X1
| X1 = X2
| X1 = X4
| ~ ron(X3,X5)
| ~ ron(X2,X5)
| X0 = X1
| ~ ron(X4,sK7(X1,X0))
| vangle(X0,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X5)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(X4)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f1823,f990]) ).
fof(f24932,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ ron(X4,sK7(X1,X0))
| ~ rpoint(X1)
| rR(X1,X2,X3)
| rR(X1,X4,X0)
| X1 = X3
| X0 = X1
| X1 = X2
| X1 = X4
| ~ ron(X3,X5)
| ~ ron(X2,X5)
| ~ rpoint(X0)
| vangle(X0,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X5)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f24925]) ).
fof(f24950,plain,
! [X2,X3,X0,X1] :
( rR(sK6,X0,sK5)
| sK6 = X1
| sK5 = sK6
| sK6 = X2
| sK6 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK6,X2,X1)
| ~ ron(X0,vd1295)
| vangle(X0,sK6,X2) = vangle(sK5,sK6,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK5)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f22016,f790]) ).
fof(f24960,plain,
! [X2,X3,X0,X1] :
( rR(sK6,X0,sK5)
| sK6 = X1
| sK6 = X2
| sK6 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK6,X2,X1)
| ~ ron(X0,vd1295)
| vangle(X0,sK6,X2) = vangle(sK5,sK6,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK5)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f24950,f788]) ).
fof(f24966,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,X3)
| sK6 = X1
| sK6 = X2
| sK6 = X0
| ~ ron(X1,X3)
| rR(sK6,X0,sK5)
| rR(sK6,X2,X1)
| ~ ron(X0,vd1295)
| vangle(X0,sK6,X2) = vangle(sK5,sK6,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f24960,f479]) ).
fof(f24992,plain,
! [X2,X3,X0,X1] :
( rR(sK4,X0,sK6)
| sK4 = X1
| sK4 = sK6
| sK4 = X2
| sK4 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK4,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK4,X2) = vangle(sK6,sK4,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK6)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f22015,f791]) ).
fof(f25001,plain,
! [X2,X3,X0,X1] :
( rR(sK4,X0,sK6)
| sK4 = X1
| sK4 = X2
| sK4 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK4,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK4,X2) = vangle(sK6,sK4,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK6)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f24992,f787]) ).
fof(f25009,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,X3)
| sK4 = X1
| sK4 = X2
| sK4 = X0
| ~ ron(X1,X3)
| rR(sK4,X0,sK6)
| rR(sK4,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK4,X2) = vangle(sK6,sK4,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f25001,f477]) ).
fof(f25053,plain,
! [X0,X1] :
( sK6 = X0
| sK4 = sK6
| sK6 = X1
| ~ ron(X0,vd1297)
| rR(sK6,X1,sK5)
| rR(sK6,sK4,X0)
| ~ ron(X1,vd1295)
| vangle(sK5,sK6,X0) = vangle(X1,sK6,sK4)
| ~ rline(vd1297)
| ~ rpoint(X0)
| ~ rpoint(sK4)
| ~ rpoint(X1) ),
inference(resolution,[],[f24966,f789]) ).
fof(f25056,plain,
! [X0,X1] :
( sK6 = X0
| sK5 = sK6
| sK6 = X1
| ~ ron(X0,vd1295)
| rR(sK6,X1,sK5)
| rR(sK6,sK5,X0)
| ~ ron(X1,vd1295)
| vangle(sK5,sK6,X0) = vangle(X1,sK6,sK5)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(X1) ),
inference(resolution,[],[f24966,f790]) ).
fof(f25077,plain,
! [X2,X3,X0,X1] :
( sK6 = X0
| sK6 = X1
| sK6 = X2
| ~ ron(X0,sK7(X3,X1))
| rR(sK6,X2,sK5)
| rR(sK6,X1,X0)
| ~ ron(X2,vd1295)
| vangle(sK5,sK6,X0) = vangle(X2,sK6,X1)
| ~ rline(sK7(X3,X1))
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rpoint(X2)
| X1 = X3
| ~ rpoint(X1)
| ~ rpoint(X3) ),
inference(resolution,[],[f24966,f990]) ).
fof(f25086,plain,
! [X2,X3,X0,X1] :
( sK6 = X0
| sK6 = X1
| sK6 = X2
| ~ ron(X0,sK7(X3,X1))
| rR(sK6,X2,sK5)
| rR(sK6,X1,X0)
| ~ ron(X2,vd1295)
| vangle(sK5,sK6,X0) = vangle(X2,sK6,X1)
| ~ rline(sK7(X3,X1))
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rpoint(X2)
| X1 = X3
| ~ rpoint(X3) ),
inference(duplicate_literal_removal,[],[f25077]) ).
fof(f25088,plain,
! [X2,X3,X0,X1] :
( ~ ron(X0,sK7(X3,X1))
| sK6 = X1
| sK6 = X2
| sK6 = X0
| rR(sK6,X2,sK5)
| rR(sK6,X1,X0)
| ~ ron(X2,vd1295)
| vangle(sK5,sK6,X0) = vangle(X2,sK6,X1)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rpoint(X2)
| X1 = X3
| ~ rpoint(X3) ),
inference(forward_subsumption_resolution,[],[f25086,f994]) ).
fof(f25091,plain,
! [X0,X1] :
( sK6 = X0
| sK6 = X1
| ~ ron(X0,vd1295)
| rR(sK6,X1,sK5)
| rR(sK6,sK5,X0)
| ~ ron(X1,vd1295)
| vangle(sK5,sK6,X0) = vangle(X1,sK6,sK5)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25056,f788]) ).
fof(f25093,plain,
! [X0,X1] :
( sK6 = X0
| sK6 = X1
| ~ ron(X0,vd1297)
| rR(sK6,X1,sK5)
| rR(sK6,sK4,X0)
| ~ ron(X1,vd1295)
| vangle(sK5,sK6,X0) = vangle(X1,sK6,sK4)
| ~ rline(vd1297)
| ~ rpoint(X0)
| ~ rpoint(sK4)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25053,f787]) ).
fof(f25103,plain,
! [X0,X1] :
( sK6 = X0
| sK6 = X1
| ~ ron(X0,vd1295)
| rR(sK6,X1,sK5)
| rR(sK6,sK5,X0)
| ~ ron(X1,vd1295)
| vangle(sK5,sK6,X0) = vangle(X1,sK6,sK5)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25091,f518]) ).
fof(f25105,plain,
! [X0,X1] :
( sK6 = X0
| sK6 = X1
| ~ ron(X0,vd1297)
| rR(sK6,X1,sK5)
| rR(sK6,sK4,X0)
| ~ ron(X1,vd1295)
| vangle(sK5,sK6,X0) = vangle(X1,sK6,sK4)
| ~ rpoint(X0)
| ~ rpoint(sK4)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25093,f515]) ).
fof(f25115,plain,
! [X0,X1] :
( rR(sK6,sK5,X0)
| rR(sK6,X1,sK5)
| ~ ron(X0,vd1295)
| sK6 = X1
| sK6 = X0
| ~ ron(X1,vd1295)
| vangle(sK5,sK6,X0) = vangle(X1,sK6,sK5)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25103,f479]) ).
fof(f25117,plain,
! [X0,X1] :
( rR(sK6,sK4,X0)
| rR(sK6,X1,sK5)
| ~ ron(X0,vd1297)
| sK6 = X1
| sK6 = X0
| ~ ron(X1,vd1295)
| vangle(sK5,sK6,X0) = vangle(X1,sK6,sK4)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25105,f481]) ).
fof(f25148,plain,
! [X0,X1] :
( sK4 = X0
| sK4 = sK6
| sK4 = X1
| ~ ron(X0,vd1295)
| rR(sK4,X1,sK6)
| rR(sK4,sK6,X0)
| ~ ron(X1,vd1297)
| vangle(sK6,sK4,X0) = vangle(X1,sK4,sK6)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(X1) ),
inference(resolution,[],[f25009,f793]) ).
fof(f25183,plain,
! [X0,X1] :
( sK4 = X0
| sK4 = X1
| ~ ron(X0,vd1295)
| rR(sK4,X1,sK6)
| rR(sK4,sK6,X0)
| ~ ron(X1,vd1297)
| vangle(sK6,sK4,X0) = vangle(X1,sK4,sK6)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25148,f787]) ).
fof(f25197,plain,
! [X0,X1] :
( sK4 = X0
| sK4 = X1
| ~ ron(X0,vd1295)
| rR(sK4,X1,sK6)
| rR(sK4,sK6,X0)
| ~ ron(X1,vd1297)
| vangle(sK6,sK4,X0) = vangle(X1,sK4,sK6)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25183,f518]) ).
fof(f25211,plain,
! [X0,X1] :
( rR(sK4,sK6,X0)
| rR(sK4,X1,sK6)
| ~ ron(X0,vd1295)
| sK4 = X1
| sK4 = X0
| ~ ron(X1,vd1297)
| vangle(sK6,sK4,X0) = vangle(X1,sK4,sK6)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25197,f477]) ).
fof(f25847,plain,
! [X2,X3,X0,X1] :
( rR(sK6,X0,sK4)
| sK6 = X1
| sK4 = sK6
| sK6 = X2
| sK6 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK6,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK6,X2) = vangle(sK4,sK6,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK4)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f22018,f789]) ).
fof(f25853,plain,
! [X2,X3,X0,X1] :
( rR(sK6,X0,sK4)
| sK6 = X1
| sK6 = X2
| sK6 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK6,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK6,X2) = vangle(sK4,sK6,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK4)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f25847,f787]) ).
fof(f25857,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,X3)
| sK6 = X1
| sK6 = X2
| sK6 = X0
| ~ ron(X1,X3)
| rR(sK6,X0,sK4)
| rR(sK6,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK6,X2) = vangle(sK4,sK6,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f25853,f481]) ).
fof(f25873,plain,
! [X0,X1] :
( sK6 = X0
| sK5 = sK6
| sK6 = X1
| ~ ron(X0,vd1295)
| rR(sK6,X1,sK4)
| rR(sK6,sK5,X0)
| ~ ron(X1,vd1297)
| vangle(sK4,sK6,X0) = vangle(X1,sK6,sK5)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(X1) ),
inference(resolution,[],[f25857,f790]) ).
fof(f25908,plain,
! [X0,X1] :
( sK6 = X0
| sK6 = X1
| ~ ron(X0,vd1295)
| rR(sK6,X1,sK4)
| rR(sK6,sK5,X0)
| ~ ron(X1,vd1297)
| vangle(sK4,sK6,X0) = vangle(X1,sK6,sK5)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25873,f788]) ).
fof(f25920,plain,
! [X0,X1] :
( sK6 = X0
| sK6 = X1
| ~ ron(X0,vd1295)
| rR(sK6,X1,sK4)
| rR(sK6,sK5,X0)
| ~ ron(X1,vd1297)
| vangle(sK4,sK6,X0) = vangle(X1,sK6,sK5)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25908,f518]) ).
fof(f25932,plain,
! [X0,X1] :
( rR(sK6,sK5,X0)
| rR(sK6,X1,sK4)
| ~ ron(X0,vd1295)
| sK6 = X1
| sK6 = X0
| ~ ron(X1,vd1297)
| vangle(sK4,sK6,X0) = vangle(X1,sK6,sK5)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25920,f479]) ).
fof(f25966,plain,
! [X0] :
( rR(sK6,X0,sK5)
| ~ ron(sK5,vd1295)
| sK6 = X0
| sK5 = sK6
| ~ ron(X0,vd1295)
| vangle(sK5,sK6,sK5) = vangle(X0,sK6,sK5)
| ~ rpoint(sK5)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(resolution,[],[f25115,f1580]) ).
fof(f25995,plain,
! [X0] :
( rR(sK6,X0,sK5)
| ~ ron(sK5,vd1295)
| sK6 = X0
| sK5 = sK6
| ~ ron(X0,vd1295)
| vangle(sK5,sK6,sK5) = vangle(X0,sK6,sK5)
| ~ rpoint(sK5)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(duplicate_literal_removal,[],[f25966]) ).
fof(f26019,plain,
! [X0] :
( rR(sK6,X0,sK5)
| sK6 = X0
| sK5 = sK6
| ~ ron(X0,vd1295)
| vangle(sK5,sK6,sK5) = vangle(X0,sK6,sK5)
| ~ rpoint(sK5)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f25995,f790]) ).
fof(f26042,plain,
! [X0] :
( rR(sK6,X0,sK5)
| sK6 = X0
| ~ ron(X0,vd1295)
| vangle(sK5,sK6,sK5) = vangle(X0,sK6,sK5)
| ~ rpoint(sK5)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f26019,f788]) ).
fof(f26059,plain,
! [X0] :
( rR(sK6,X0,sK5)
| sK6 = X0
| ~ ron(X0,vd1295)
| vangle(sK5,sK6,sK5) = vangle(X0,sK6,sK5)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f26042,f479]) ).
fof(f26068,plain,
! [X0] :
( rR(sK6,X0,sK5)
| sK6 = X0
| ~ ron(X0,vd1295)
| vangle(sK5,sK6,sK5) = vangle(X0,sK6,sK5)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26059,f477]) ).
fof(f26075,definition,
( spl54_1090
<=> rR(sK5,vd1300,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_1090])],[avatar_definition]) ).
fof(f26077,plain,
( rR(sK5,vd1300,sK5)
| ~ spl54_1090 ),
inference(avatar_component_clause,[],[f26075]) ).
fof(f26082,plain,
! [X0] :
( rR(sK6,X0,sK5)
| vd684 = vangle(X0,sK6,sK5)
| sK6 = X0
| ~ ron(X0,vd1295)
| ~ rpoint(X0) ),
inference(forward_demodulation,[],[f26068,f1850]) ).
fof(f26087,definition,
( spl54_1092
<=> rR(sK6,vd1300,sK6) ),
introduced(definition,[new_symbols(definition,[spl54_1092])],[avatar_definition]) ).
fof(f26088,plain,
( ~ rR(sK6,vd1300,sK6)
| spl54_1092 ),
inference(avatar_component_clause,[],[f26087]) ).
fof(f26089,plain,
( rR(sK6,vd1300,sK6)
| ~ spl54_1092 ),
inference(avatar_component_clause,[],[f26087]) ).
fof(f26110,plain,
( vd684 = vangle(vd1300,sK6,sK5)
| vd1300 = sK6
| ~ ron(vd1300,vd1295)
| ~ rpoint(vd1300)
| rR(sK6,vd1300,sK6)
| ~ rpoint(sK6) ),
inference(resolution,[],[f26082,f1733]) ).
fof(f26180,plain,
! [X0] :
( rR(sK6,sK4,X0)
| ~ ron(X0,vd1297)
| sK5 = sK6
| sK6 = X0
| ~ ron(sK5,vd1295)
| vangle(sK5,sK6,sK4) = vangle(sK5,sK6,X0)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(resolution,[],[f25117,f1580]) ).
fof(f26183,plain,
! [X0] :
( rR(sK6,sK4,X0)
| ~ ron(X0,vd1297)
| sK5 = sK6
| sK6 = X0
| ~ ron(sK5,vd1295)
| vangle(sK5,sK6,sK4) = vangle(sK5,sK6,X0)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(duplicate_literal_removal,[],[f26180]) ).
fof(f26207,plain,
! [X0] :
( rR(sK6,sK4,X0)
| ~ ron(X0,vd1297)
| sK6 = X0
| ~ ron(sK5,vd1295)
| vangle(sK5,sK6,sK4) = vangle(sK5,sK6,X0)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f26183,f788]) ).
fof(f26231,plain,
! [X0] :
( rR(sK6,sK4,X0)
| ~ ron(X0,vd1297)
| sK6 = X0
| vangle(sK5,sK6,sK4) = vangle(sK5,sK6,X0)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f26207,f790]) ).
fof(f26255,plain,
! [X0] :
( rR(sK6,sK4,X0)
| ~ ron(X0,vd1297)
| sK6 = X0
| vangle(sK5,sK6,sK4) = vangle(sK5,sK6,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f26231,f479]) ).
fof(f26267,plain,
! [X0] :
( rR(sK6,sK4,X0)
| ~ ron(X0,vd1297)
| sK6 = X0
| vangle(sK5,sK6,sK4) = vangle(sK5,sK6,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26255,f477]) ).
fof(f26274,plain,
! [X0] :
( vangle(sK4,sK6,sK5) = vangle(sK5,sK6,X0)
| rR(sK6,sK4,X0)
| ~ ron(X0,vd1297)
| sK6 = X0
| ~ rpoint(X0) ),
inference(forward_demodulation,[],[f26267,f2248]) ).
fof(f26277,definition,
( spl54_1094
<=> ! [X0] :
( vangle(sK4,sK6,sK5) = vangle(sK5,sK6,X0)
| ~ rpoint(X0)
| sK6 = X0
| ~ ron(X0,vd1297)
| rR(sK6,sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_1094])],[avatar_definition]) ).
fof(f26278,plain,
( ! [X0] :
( rR(sK6,sK4,X0)
| ~ rpoint(X0)
| sK6 = X0
| ~ ron(X0,vd1297)
| vangle(sK4,sK6,sK5) = vangle(sK5,sK6,X0) )
| ~ spl54_1094 ),
inference(avatar_component_clause,[],[f26277]) ).
fof(f26282,plain,
spl54_1094,
inference(avatar_split_clause,[],[f26274,f26277]) ).
fof(f26287,plain,
! [X2,X3,X0,X1,X4] :
( ~ rpoint(X0)
| rR(X0,X1,X2)
| rR(X0,X3,X3)
| X0 = X2
| X0 = X3
| X0 = X1
| X0 = X3
| ~ ron(X2,X4)
| ~ ron(X1,X4)
| ~ rpoint(X3)
| vangle(X3,X0,X2) = vangle(X3,X0,X1)
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X3)
| X0 = X3
| ~ rpoint(X3)
| ~ rpoint(X0) ),
inference(resolution,[],[f24932,f990]) ).
fof(f26294,plain,
! [X2,X3,X0,X1,X4] :
( ~ rpoint(X0)
| rR(X0,X1,X2)
| rR(X0,X3,X3)
| X0 = X2
| X0 = X3
| X0 = X1
| ~ ron(X2,X4)
| ~ ron(X1,X4)
| ~ rpoint(X3)
| vangle(X3,X0,X2) = vangle(X3,X0,X1)
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(duplicate_literal_removal,[],[f26287]) ).
fof(f26299,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X2,X4)
| rR(X0,X1,X2)
| X0 = X2
| X0 = X3
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,X4)
| ~ rpoint(X3)
| vangle(X3,X0,X2) = vangle(X3,X0,X1)
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26294,f1580]) ).
fof(f26319,plain,
! [X2,X0,X1] :
( rR(X0,X1,sK4)
| sK4 = X0
| X0 = X2
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,vd1297)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,sK4)
| ~ rline(vd1297)
| ~ rpoint(sK4)
| ~ rpoint(X1) ),
inference(resolution,[],[f26299,f789]) ).
fof(f26362,plain,
! [X2,X0,X1] :
( rR(X0,X1,sK4)
| sK4 = X0
| X0 = X2
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,vd1297)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,sK4)
| ~ rpoint(sK4)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26319,f515]) ).
fof(f26377,plain,
! [X2,X0,X1] :
( ~ ron(X1,vd1297)
| sK4 = X0
| X0 = X2
| X0 = X1
| ~ rpoint(X0)
| rR(X0,X1,sK4)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,sK4)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26362,f481]) ).
fof(f26430,plain,
( rR(sK6,sK6,vd1300)
| ~ rpoint(sK6)
| ~ rpoint(sK6)
| ~ rpoint(vd1300)
| ~ spl54_1092 ),
inference(resolution,[],[f26089,f979]) ).
fof(f26443,plain,
( rR(sK6,sK6,vd1300)
| ~ rpoint(sK6)
| ~ rpoint(vd1300)
| ~ spl54_1092 ),
inference(duplicate_literal_removal,[],[f26430]) ).
fof(f26450,plain,
( ~ rpoint(sK6)
| ~ rpoint(vd1300)
| ~ spl54_1092 ),
inference(forward_subsumption_resolution,[],[f26443,f1579]) ).
fof(f26454,plain,
( ~ rpoint(vd1300)
| ~ spl54_1092 ),
inference(forward_subsumption_resolution,[],[f26450,f477]) ).
fof(f26458,plain,
( $false
| ~ spl54_1092 ),
inference(forward_subsumption_resolution,[],[f26454,f547]) ).
fof(f26459,plain,
~ spl54_1092,
inference(avatar_contradiction_clause,[],[f26458]) ).
fof(f26462,plain,
( vd684 = vangle(vd1300,sK6,sK5)
| ~ ron(vd1300,vd1295)
| ~ rpoint(vd1300)
| rR(sK6,vd1300,sK6)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f26110,f794]) ).
fof(f26464,plain,
( vd684 = vangle(vd1300,sK6,sK5)
| ~ rpoint(vd1300)
| rR(sK6,vd1300,sK6)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f26462,f792]) ).
fof(f26466,plain,
( vd684 = vangle(vd1300,sK6,sK5)
| rR(sK6,vd1300,sK6)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f26464,f547]) ).
fof(f26468,plain,
( vd684 = vangle(vd1300,sK6,sK5)
| ~ rpoint(sK6)
| spl54_1092 ),
inference(forward_subsumption_resolution,[],[f26466,f26088]) ).
fof(f26470,plain,
( vd684 = vangle(vd1300,sK6,sK5)
| spl54_1092 ),
inference(forward_subsumption_resolution,[],[f26468,f477]) ).
fof(f26472,plain,
( vd684 = vangle(sK5,sK6,vd1300)
| spl54_15
| spl54_1092 ),
inference(forward_demodulation,[],[f26470,f2499]) ).
fof(f28230,plain,
! [X0] :
( rR(sK4,X0,sK6)
| ~ ron(sK5,vd1295)
| sK4 = X0
| sK4 = sK5
| ~ ron(X0,vd1297)
| vangle(sK6,sK4,sK5) = vangle(X0,sK4,sK6)
| ~ rpoint(sK5)
| ~ rpoint(X0)
| rR(sK4,sK6,vd1300)
| ~ rpoint(sK4) ),
inference(resolution,[],[f25211,f1736]) ).
fof(f28304,plain,
! [X0] :
( rR(sK4,X0,sK6)
| sK4 = X0
| sK4 = sK5
| ~ ron(X0,vd1297)
| vangle(sK6,sK4,sK5) = vangle(X0,sK4,sK6)
| ~ rpoint(sK5)
| ~ rpoint(X0)
| rR(sK4,sK6,vd1300)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f28230,f790]) ).
fof(f28325,plain,
! [X0] :
( rR(sK4,X0,sK6)
| sK4 = X0
| ~ ron(X0,vd1297)
| vangle(sK6,sK4,sK5) = vangle(X0,sK4,sK6)
| ~ rpoint(sK5)
| ~ rpoint(X0)
| rR(sK4,sK6,vd1300)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f28304,f763]) ).
fof(f28333,plain,
! [X0] :
( rR(sK4,X0,sK6)
| sK4 = X0
| ~ ron(X0,vd1297)
| vangle(sK6,sK4,sK5) = vangle(X0,sK4,sK6)
| ~ rpoint(X0)
| rR(sK4,sK6,vd1300)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f28325,f479]) ).
fof(f28338,plain,
! [X0] :
( rR(sK4,X0,sK6)
| sK4 = X0
| ~ ron(X0,vd1297)
| vangle(sK6,sK4,sK5) = vangle(X0,sK4,sK6)
| ~ rpoint(X0)
| rR(sK4,sK6,vd1300) ),
inference(forward_subsumption_resolution,[],[f28333,f481]) ).
fof(f28342,plain,
! [X0] :
( sF52 = vangle(X0,sK4,sK6)
| rR(sK4,X0,sK6)
| sK4 = X0
| ~ ron(X0,vd1297)
| ~ rpoint(X0)
| rR(sK4,sK6,vd1300) ),
inference(forward_demodulation,[],[f28338,f1574]) ).
fof(f28344,definition,
( spl54_1277
<=> rR(sK4,sK6,vd1300) ),
introduced(definition,[new_symbols(definition,[spl54_1277])],[avatar_definition]) ).
fof(f28346,plain,
( rR(sK4,sK6,vd1300)
| ~ spl54_1277 ),
inference(avatar_component_clause,[],[f28344]) ).
fof(f28348,definition,
( spl54_1278
<=> ! [X0] :
( sF52 = vangle(X0,sK4,sK6)
| ~ rpoint(X0)
| ~ ron(X0,vd1297)
| sK4 = X0
| rR(sK4,X0,sK6) ) ),
introduced(definition,[new_symbols(definition,[spl54_1278])],[avatar_definition]) ).
fof(f28349,plain,
( ! [X0] :
( rR(sK4,X0,sK6)
| ~ rpoint(X0)
| ~ ron(X0,vd1297)
| sK4 = X0
| sF52 = vangle(X0,sK4,sK6) )
| ~ spl54_1278 ),
inference(avatar_component_clause,[],[f28348]) ).
fof(f28350,plain,
( spl54_1277
| spl54_1278 ),
inference(avatar_split_clause,[],[f28342,f28348,f28344]) ).
fof(f28354,plain,
( ~ rR(sK6,sK4,vd1300)
| ~ rpoint(vd1300)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ spl54_1277 ),
inference(resolution,[],[f28346,f968]) ).
fof(f28368,plain,
( ~ rR(sK6,sK4,vd1300)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f28354,f547]) ).
fof(f28377,plain,
( ~ rR(sK6,sK4,vd1300)
| ~ rpoint(sK4)
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f28368,f477]) ).
fof(f28385,plain,
( ~ rR(sK6,sK4,vd1300)
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f28377,f481]) ).
fof(f28391,plain,
( ~ rpoint(sK6)
| ~ ron(sK6,vd1297)
| sK4 = sK6
| sF52 = vangle(sK6,sK4,sK6)
| ~ rR(sK4,vd1303,sK6)
| ~ rpoint(sK6)
| ~ spl54_1278 ),
inference(resolution,[],[f28349,f2129]) ).
fof(f28416,plain,
( ~ rpoint(sK6)
| ~ ron(sK6,vd1297)
| sK4 = sK6
| sF52 = vangle(sK6,sK4,sK6)
| ~ rR(sK4,vd1303,sK6)
| ~ spl54_1278 ),
inference(duplicate_literal_removal,[],[f28391]) ).
fof(f28426,plain,
( ~ ron(sK6,vd1297)
| sK4 = sK6
| sF52 = vangle(sK6,sK4,sK6)
| ~ rR(sK4,vd1303,sK6)
| ~ spl54_1278 ),
inference(forward_subsumption_resolution,[],[f28416,f477]) ).
fof(f28436,plain,
( sK4 = sK6
| sF52 = vangle(sK6,sK4,sK6)
| ~ rR(sK4,vd1303,sK6)
| ~ spl54_1278 ),
inference(forward_subsumption_resolution,[],[f28426,f791]) ).
fof(f28440,plain,
( sF52 = vangle(sK6,sK4,sK6)
| ~ rR(sK4,vd1303,sK6)
| ~ spl54_1278 ),
inference(forward_subsumption_resolution,[],[f28436,f787]) ).
fof(f28442,plain,
( sF52 = vangle(sK6,sK4,sK6)
| ~ spl54_1278 ),
inference(forward_subsumption_resolution,[],[f28440,f1636]) ).
fof(f28444,plain,
( vd684 = sF52
| ~ spl54_1278 ),
inference(forward_demodulation,[],[f28442,f1879]) ).
fof(f28447,plain,
( $false
| spl54_732
| ~ spl54_1278 ),
inference(forward_subsumption_resolution,[],[f28444,f20687]) ).
fof(f28448,plain,
( spl54_732
| ~ spl54_1278 ),
inference(avatar_contradiction_clause,[],[f28447]) ).
fof(f28944,plain,
! [X0] :
( rR(sK6,X0,sK4)
| ~ ron(sK5,vd1295)
| sK6 = X0
| sK5 = sK6
| ~ ron(X0,vd1297)
| vangle(sK4,sK6,sK5) = vangle(X0,sK6,sK5)
| ~ rpoint(sK5)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(resolution,[],[f25932,f1580]) ).
fof(f28969,plain,
! [X0] :
( rR(sK6,X0,sK4)
| ~ ron(sK5,vd1295)
| sK6 = X0
| sK5 = sK6
| ~ ron(X0,vd1297)
| vangle(sK4,sK6,sK5) = vangle(X0,sK6,sK5)
| ~ rpoint(sK5)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(duplicate_literal_removal,[],[f28944]) ).
fof(f28991,plain,
! [X0] :
( rR(sK6,X0,sK4)
| sK6 = X0
| sK5 = sK6
| ~ ron(X0,vd1297)
| vangle(sK4,sK6,sK5) = vangle(X0,sK6,sK5)
| ~ rpoint(sK5)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f28969,f790]) ).
fof(f29012,plain,
! [X0] :
( rR(sK6,X0,sK4)
| sK6 = X0
| ~ ron(X0,vd1297)
| vangle(sK4,sK6,sK5) = vangle(X0,sK6,sK5)
| ~ rpoint(sK5)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f28991,f788]) ).
fof(f29026,plain,
! [X0] :
( rR(sK6,X0,sK4)
| sK6 = X0
| ~ ron(X0,vd1297)
| vangle(sK4,sK6,sK5) = vangle(X0,sK6,sK5)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f29012,f479]) ).
fof(f29033,plain,
! [X0] :
( rR(sK6,X0,sK4)
| sK6 = X0
| ~ ron(X0,vd1297)
| vangle(sK4,sK6,sK5) = vangle(X0,sK6,sK5)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f29026,f477]) ).
fof(f29039,definition,
( spl54_1280
<=> rR(sK6,vd1303,sK6) ),
introduced(definition,[new_symbols(definition,[spl54_1280])],[avatar_definition]) ).
fof(f29040,plain,
( ~ rR(sK6,vd1303,sK6)
| spl54_1280 ),
inference(avatar_component_clause,[],[f29039]) ).
fof(f29041,plain,
( rR(sK6,vd1303,sK6)
| ~ spl54_1280 ),
inference(avatar_component_clause,[],[f29039]) ).
fof(f29506,definition,
( spl54_1284
<=> rR(sK5,sK6,vd1303) ),
introduced(definition,[new_symbols(definition,[spl54_1284])],[avatar_definition]) ).
fof(f29508,plain,
( rR(sK5,sK6,vd1303)
| ~ spl54_1284 ),
inference(avatar_component_clause,[],[f29506]) ).
fof(f29520,plain,
( ~ rR(sK6,sK5,vd1303)
| ~ rpoint(vd1303)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ spl54_1284 ),
inference(resolution,[],[f29508,f968]) ).
fof(f29534,plain,
( ~ rR(sK6,sK5,vd1303)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ spl54_1284 ),
inference(forward_subsumption_resolution,[],[f29520,f510]) ).
fof(f29543,plain,
( ~ rR(sK6,sK5,vd1303)
| ~ rpoint(sK5)
| ~ spl54_1284 ),
inference(forward_subsumption_resolution,[],[f29534,f477]) ).
fof(f29551,plain,
( ~ rR(sK6,sK5,vd1303)
| ~ spl54_1284 ),
inference(forward_subsumption_resolution,[],[f29543,f479]) ).
fof(f29753,plain,
( vd1303 = sK6
| ~ ron(vd1303,vd1297)
| vangle(sK4,sK6,sK5) = vangle(vd1303,sK6,sK5)
| ~ rpoint(vd1303)
| rR(sK6,vd1303,sK6)
| ~ rpoint(sK6) ),
inference(resolution,[],[f29033,f1732]) ).
fof(f29789,plain,
( rR(sK6,sK6,vd1303)
| ~ rpoint(sK6)
| ~ rpoint(sK6)
| ~ rpoint(vd1303)
| ~ spl54_1280 ),
inference(resolution,[],[f29041,f979]) ).
fof(f29802,plain,
( rR(sK6,sK6,vd1303)
| ~ rpoint(sK6)
| ~ rpoint(vd1303)
| ~ spl54_1280 ),
inference(duplicate_literal_removal,[],[f29789]) ).
fof(f29809,plain,
( ~ rpoint(sK6)
| ~ rpoint(vd1303)
| ~ spl54_1280 ),
inference(forward_subsumption_resolution,[],[f29802,f1579]) ).
fof(f29813,plain,
( ~ rpoint(vd1303)
| ~ spl54_1280 ),
inference(forward_subsumption_resolution,[],[f29809,f477]) ).
fof(f29817,plain,
( $false
| ~ spl54_1280 ),
inference(forward_subsumption_resolution,[],[f29813,f510]) ).
fof(f29818,plain,
~ spl54_1280,
inference(avatar_contradiction_clause,[],[f29817]) ).
fof(f29822,plain,
( ~ ron(vd1303,vd1297)
| vangle(sK4,sK6,sK5) = vangle(vd1303,sK6,sK5)
| ~ rpoint(vd1303)
| rR(sK6,vd1303,sK6)
| ~ rpoint(sK6)
| spl54_18 ),
inference(forward_subsumption_resolution,[],[f29753,f1859]) ).
fof(f29825,plain,
( vangle(sK4,sK6,sK5) = vangle(vd1303,sK6,sK5)
| ~ rpoint(vd1303)
| rR(sK6,vd1303,sK6)
| ~ rpoint(sK6)
| spl54_18 ),
inference(forward_subsumption_resolution,[],[f29822,f776]) ).
fof(f29828,plain,
( vangle(sK4,sK6,sK5) = vangle(vd1303,sK6,sK5)
| rR(sK6,vd1303,sK6)
| ~ rpoint(sK6)
| spl54_18 ),
inference(forward_subsumption_resolution,[],[f29825,f510]) ).
fof(f29831,plain,
( vangle(sK4,sK6,sK5) = vangle(vd1303,sK6,sK5)
| ~ rpoint(sK6)
| spl54_18
| spl54_1280 ),
inference(forward_subsumption_resolution,[],[f29828,f29040]) ).
fof(f29834,plain,
( vangle(sK4,sK6,sK5) = vangle(vd1303,sK6,sK5)
| spl54_18
| spl54_1280 ),
inference(forward_subsumption_resolution,[],[f29831,f477]) ).
fof(f29837,plain,
( vangle(sK4,sK6,sK5) = vangle(sK5,sK6,vd1303)
| spl54_18
| spl54_25
| spl54_1280 ),
inference(forward_demodulation,[],[f29834,f13805]) ).
fof(f29839,plain,
! [X2,X0,X1] :
( sK6 = X0
| sK6 = X1
| sK6 = X2
| rR(sK6,X1,sK5)
| rR(sK6,X0,X2)
| ~ ron(X1,vd1295)
| vangle(X1,sK6,X0) = vangle(sK5,sK6,X2)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X2
| ~ rpoint(X2)
| X0 = X2
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(resolution,[],[f25088,f992]) ).
fof(f29844,plain,
! [X2,X0,X1] :
( rR(sK6,X1,sK5)
| rR(sK6,X0,X2)
| sK6 = X2
| sK6 = X1
| sK6 = X0
| ~ ron(X1,vd1295)
| vangle(X1,sK6,X0) = vangle(sK5,sK6,X2)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X2 ),
inference(duplicate_literal_removal,[],[f29839]) ).
fof(f31458,plain,
! [X0,X1] :
( sK4 = X0
| X0 = X1
| sK6 = X0
| ~ rpoint(X0)
| rR(X0,sK6,sK4)
| ~ rpoint(X1)
| vangle(X1,X0,sK6) = vangle(X1,X0,sK4)
| ~ rpoint(sK6) ),
inference(resolution,[],[f26377,f791]) ).
fof(f31464,plain,
! [X0,X1] :
( ~ rpoint(X1)
| X0 = X1
| sK6 = X0
| ~ rpoint(X0)
| rR(X0,sK6,sK4)
| sK4 = X0
| vangle(X1,X0,sK6) = vangle(X1,X0,sK4) ),
inference(forward_subsumption_resolution,[],[f31458,f477]) ).
fof(f32691,plain,
! [X0] :
( sK6 = X0
| sK6 = X0
| ~ rpoint(X0)
| rR(X0,sK6,sK4)
| sK4 = X0
| vangle(sK6,X0,sK4) = vangle(sK6,X0,sK6) ),
inference(resolution,[],[f31464,f477]) ).
fof(f32692,plain,
! [X0] :
( rR(X0,sK6,sK4)
| ~ rpoint(X0)
| sK6 = X0
| sK4 = X0
| vangle(sK6,X0,sK4) = vangle(sK6,X0,sK6) ),
inference(duplicate_literal_removal,[],[f32691]) ).
fof(f33853,plain,
( ~ rpoint(vd1303)
| vd1303 = sK6
| ~ ron(vd1303,vd1297)
| vangle(sK4,sK6,sK5) = vangle(sK5,sK6,vd1303)
| ~ spl54_1094 ),
inference(resolution,[],[f26278,f1689]) ).
fof(f34015,plain,
( ~ rpoint(sK5)
| sK5 = sK6
| sK4 = sK5
| vangle(sK6,sK5,sK4) = vangle(sK6,sK5,sK6)
| ~ rR(sK5,vd1300,sK4)
| ~ rpoint(sK4) ),
inference(resolution,[],[f32692,f2132]) ).
fof(f34029,plain,
( sK5 = sK6
| sK4 = sK5
| vangle(sK6,sK5,sK4) = vangle(sK6,sK5,sK6)
| ~ rR(sK5,vd1300,sK4)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f34015,f479]) ).
fof(f34039,plain,
( sK4 = sK5
| vangle(sK6,sK5,sK4) = vangle(sK6,sK5,sK6)
| ~ rR(sK5,vd1300,sK4)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f34029,f788]) ).
fof(f34049,plain,
( vangle(sK6,sK5,sK4) = vangle(sK6,sK5,sK6)
| ~ rR(sK5,vd1300,sK4)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f34039,f763]) ).
fof(f34052,plain,
( vangle(sK6,sK5,sK4) = vangle(sK6,sK5,sK6)
| ~ rR(sK5,vd1300,sK4) ),
inference(forward_subsumption_resolution,[],[f34049,f481]) ).
fof(f34055,plain,
( vd684 = vangle(sK6,sK5,sK4)
| ~ rR(sK5,vd1300,sK4) ),
inference(forward_demodulation,[],[f34052,f2017]) ).
fof(f34056,plain,
( vd684 = sF53
| ~ rR(sK5,vd1300,sK4) ),
inference(forward_demodulation,[],[f34055,f1576]) ).
fof(f34057,plain,
( ~ rR(sK5,vd1300,sK4)
| spl54_730 ),
inference(forward_subsumption_resolution,[],[f34056,f20343]) ).
fof(f34058,plain,
( ~ spl54_1075
| spl54_730 ),
inference(avatar_split_clause,[],[f34057,f20341,f24846]) ).
fof(f36464,plain,
! [X0,X1] :
( rR(sK6,X0,X1)
| sK6 = X1
| sK5 = sK6
| sK6 = X0
| ~ ron(sK5,vd1295)
| vangle(sK5,sK6,X0) = vangle(sK5,sK6,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| X0 = X1
| rR(sK5,vd1300,sK5)
| ~ rpoint(sK5) ),
inference(resolution,[],[f29844,f1758]) ).
fof(f36487,plain,
( ! [X0] :
( rR(sK6,X0,sK5)
| vd1300 = sK6
| sK6 = X0
| sK4 = sK6
| ~ ron(X0,vd1295)
| vangle(X0,sK6,sK4) = vangle(sK5,sK6,vd1300)
| ~ rpoint(vd1300)
| ~ rpoint(sK4)
| ~ rpoint(X0)
| vd1300 = sK4 )
| ~ spl54_1277 ),
inference(resolution,[],[f29844,f28385]) ).
fof(f36544,plain,
! [X0,X1] :
( rR(sK6,X0,X1)
| sK6 = X1
| sK5 = sK6
| sK6 = X0
| ~ ron(sK5,vd1295)
| vangle(sK5,sK6,X0) = vangle(sK5,sK6,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| X0 = X1
| rR(sK5,vd1300,sK5) ),
inference(duplicate_literal_removal,[],[f36464]) ).
fof(f36560,plain,
( ! [X0] :
( rR(sK6,X0,sK5)
| sK6 = X0
| sK4 = sK6
| ~ ron(X0,vd1295)
| vangle(X0,sK6,sK4) = vangle(sK5,sK6,vd1300)
| ~ rpoint(vd1300)
| ~ rpoint(sK4)
| ~ rpoint(X0)
| vd1300 = sK4 )
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f36487,f794]) ).
fof(f36575,plain,
! [X0,X1] :
( rR(sK6,X0,X1)
| sK6 = X1
| sK6 = X0
| ~ ron(sK5,vd1295)
| vangle(sK5,sK6,X0) = vangle(sK5,sK6,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| X0 = X1
| rR(sK5,vd1300,sK5) ),
inference(forward_subsumption_resolution,[],[f36544,f788]) ).
fof(f36584,plain,
( ! [X0] :
( rR(sK6,X0,sK5)
| sK6 = X0
| ~ ron(X0,vd1295)
| vangle(X0,sK6,sK4) = vangle(sK5,sK6,vd1300)
| ~ rpoint(vd1300)
| ~ rpoint(sK4)
| ~ rpoint(X0)
| vd1300 = sK4 )
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f36560,f787]) ).
fof(f36599,plain,
! [X0,X1] :
( rR(sK6,X0,X1)
| sK6 = X1
| sK6 = X0
| vangle(sK5,sK6,X0) = vangle(sK5,sK6,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| X0 = X1
| rR(sK5,vd1300,sK5) ),
inference(forward_subsumption_resolution,[],[f36575,f790]) ).
fof(f36605,plain,
( ! [X0] :
( rR(sK6,X0,sK5)
| sK6 = X0
| ~ ron(X0,vd1295)
| vangle(X0,sK6,sK4) = vangle(sK5,sK6,vd1300)
| ~ rpoint(sK4)
| ~ rpoint(X0)
| vd1300 = sK4 )
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f36584,f547]) ).
fof(f36612,plain,
! [X0,X1] :
( rR(sK6,X0,X1)
| sK6 = X1
| sK6 = X0
| vangle(sK5,sK6,X0) = vangle(sK5,sK6,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X1
| rR(sK5,vd1300,sK5) ),
inference(forward_subsumption_resolution,[],[f36599,f479]) ).
fof(f36617,plain,
( ! [X0] :
( rR(sK6,X0,sK5)
| sK6 = X0
| ~ ron(X0,vd1295)
| vangle(X0,sK6,sK4) = vangle(sK5,sK6,vd1300)
| ~ rpoint(X0)
| vd1300 = sK4 )
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f36605,f481]) ).
fof(f36623,definition,
( spl54_1337
<=> ! [X0,X1] :
( rR(sK6,X0,X1)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| vangle(sK5,sK6,X0) = vangle(sK5,sK6,X1)
| sK6 = X0
| sK6 = X1 ) ),
introduced(definition,[new_symbols(definition,[spl54_1337])],[avatar_definition]) ).
fof(f36624,plain,
( ! [X0,X1] :
( rR(sK6,X0,X1)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| vangle(sK5,sK6,X0) = vangle(sK5,sK6,X1)
| sK6 = X0
| sK6 = X1 )
| ~ spl54_1337 ),
inference(avatar_component_clause,[],[f36623]) ).
fof(f36625,plain,
( spl54_1090
| spl54_1337 ),
inference(avatar_split_clause,[],[f36612,f36623,f26075]) ).
fof(f36630,plain,
( ! [X0] :
( rR(sK6,X0,sK5)
| sK6 = X0
| ~ ron(X0,vd1295)
| vangle(X0,sK6,sK4) = vangle(sK5,sK6,vd1300)
| ~ rpoint(X0) )
| spl54_13
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f36617,f1767]) ).
fof(f36639,plain,
( ! [X0] :
( rR(sK6,X0,sK5)
| vd684 = vangle(X0,sK6,sK4)
| sK6 = X0
| ~ ron(X0,vd1295)
| ~ rpoint(X0) )
| spl54_13
| spl54_15
| spl54_1092
| ~ spl54_1277 ),
inference(forward_demodulation,[],[f36630,f26472]) ).
fof(f36661,plain,
( vd1303 = sK5
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| vangle(sK5,sK6,sK5) = vangle(sK5,sK6,vd1303)
| sK5 = sK6
| vd1303 = sK6
| ~ spl54_1284
| ~ spl54_1337 ),
inference(resolution,[],[f36624,f29551]) ).
fof(f36713,plain,
( ~ rpoint(sK5)
| ~ rpoint(vd1303)
| vangle(sK5,sK6,sK5) = vangle(sK5,sK6,vd1303)
| sK5 = sK6
| vd1303 = sK6
| spl54_25
| ~ spl54_1284
| ~ spl54_1337 ),
inference(forward_subsumption_resolution,[],[f36661,f2025]) ).
fof(f36726,plain,
( ~ rpoint(vd1303)
| vangle(sK5,sK6,sK5) = vangle(sK5,sK6,vd1303)
| sK5 = sK6
| vd1303 = sK6
| spl54_25
| ~ spl54_1284
| ~ spl54_1337 ),
inference(forward_subsumption_resolution,[],[f36713,f479]) ).
fof(f36737,plain,
( vangle(sK5,sK6,sK5) = vangle(sK5,sK6,vd1303)
| sK5 = sK6
| vd1303 = sK6
| spl54_25
| ~ spl54_1284
| ~ spl54_1337 ),
inference(forward_subsumption_resolution,[],[f36726,f510]) ).
fof(f36748,plain,
( vangle(sK5,sK6,sK5) = vangle(sK5,sK6,vd1303)
| vd1303 = sK6
| spl54_25
| ~ spl54_1284
| ~ spl54_1337 ),
inference(forward_subsumption_resolution,[],[f36737,f788]) ).
fof(f36757,plain,
( vangle(sK5,sK6,sK5) = vangle(sK5,sK6,vd1303)
| spl54_18
| spl54_25
| ~ spl54_1284
| ~ spl54_1337 ),
inference(forward_subsumption_resolution,[],[f36748,f1859]) ).
fof(f36765,plain,
( vangle(sK5,sK6,sK5) = vangle(sK4,sK6,sK5)
| spl54_18
| spl54_25
| spl54_1280
| ~ spl54_1284
| ~ spl54_1337 ),
inference(forward_demodulation,[],[f36757,f29837]) ).
fof(f36772,plain,
( vd684 = vangle(sK4,sK6,sK5)
| spl54_18
| spl54_25
| spl54_1280
| ~ spl54_1284
| ~ spl54_1337 ),
inference(forward_demodulation,[],[f36765,f1850]) ).
fof(f36778,plain,
( $false
| spl54_18
| spl54_25
| spl54_738
| spl54_1280
| ~ spl54_1284
| ~ spl54_1337 ),
inference(forward_subsumption_resolution,[],[f36772,f21162]) ).
fof(f36779,plain,
( spl54_18
| spl54_25
| spl54_738
| spl54_1280
| ~ spl54_1284
| ~ spl54_1337 ),
inference(avatar_contradiction_clause,[],[f36778]) ).
fof(f36915,plain,
( vd684 = vangle(vd1300,sK6,sK4)
| vd1300 = sK6
| ~ ron(vd1300,vd1295)
| ~ rpoint(vd1300)
| rR(sK6,vd1300,sK6)
| ~ rpoint(sK6)
| spl54_13
| spl54_15
| spl54_1092
| ~ spl54_1277 ),
inference(resolution,[],[f36639,f1733]) ).
fof(f36931,plain,
( vd684 = vangle(vd1300,sK6,sK4)
| ~ ron(vd1300,vd1295)
| ~ rpoint(vd1300)
| rR(sK6,vd1300,sK6)
| ~ rpoint(sK6)
| spl54_13
| spl54_15
| spl54_1092
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f36915,f794]) ).
fof(f36942,plain,
( vd684 = vangle(vd1300,sK6,sK4)
| ~ rpoint(vd1300)
| rR(sK6,vd1300,sK6)
| ~ rpoint(sK6)
| spl54_13
| spl54_15
| spl54_1092
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f36931,f792]) ).
fof(f36953,plain,
( vd684 = vangle(vd1300,sK6,sK4)
| rR(sK6,vd1300,sK6)
| ~ rpoint(sK6)
| spl54_13
| spl54_15
| spl54_1092
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f36942,f547]) ).
fof(f36958,plain,
( vd684 = vangle(vd1300,sK6,sK4)
| ~ rpoint(sK6)
| spl54_13
| spl54_15
| spl54_1092
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f36953,f26088]) ).
fof(f36961,plain,
( vd684 = vangle(vd1300,sK6,sK4)
| spl54_13
| spl54_15
| spl54_1092
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f36958,f477]) ).
fof(f36963,plain,
( vd684 = vangle(sK5,sK6,sK4)
| spl54_13
| spl54_15
| spl54_1092
| ~ spl54_1277 ),
inference(forward_demodulation,[],[f36961,f767]) ).
fof(f36964,plain,
( vd684 = vangle(sK4,sK6,sK5)
| spl54_13
| spl54_15
| spl54_1092
| ~ spl54_1277 ),
inference(forward_demodulation,[],[f36963,f2248]) ).
fof(f37044,plain,
! [X2,X3,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X2
| ~ ron(X2,sK15(X1,X0))
| X0 = X1
| rR(X1,X0,X2)
| ~ ron(X2,X3)
| ~ ron(X0,X3)
| ~ ron(X1,X3)
| ~ rline(X3)
| ~ rpoint(X2)
| ~ rpoint(X0)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f4227,f1106]) ).
fof(f37057,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,sK15(X1,X0))
| ~ rpoint(X1)
| X0 = X2
| ~ rpoint(X0)
| X0 = X1
| rR(X1,X0,X2)
| ~ ron(X2,X3)
| ~ ron(X0,X3)
| ~ ron(X1,X3)
| ~ rline(X3)
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f37044]) ).
fof(f37107,plain,
! [X0] :
( ~ rpoint(sK6)
| sK4 = sK5
| ~ rpoint(sK4)
| sK4 = sK6
| rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5) ),
inference(resolution,[],[f37057,f7275]) ).
fof(f37122,plain,
! [X0] :
( sK4 = sK5
| ~ rpoint(sK4)
| sK4 = sK6
| rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f37107,f477]) ).
fof(f37129,plain,
! [X0] :
( ~ rpoint(sK4)
| sK4 = sK6
| rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f37122,f763]) ).
fof(f37136,plain,
! [X0] :
( sK4 = sK6
| rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f37129,f481]) ).
fof(f37143,plain,
! [X0] :
( rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f37136,f787]) ).
fof(f37150,plain,
! [X0] :
( rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f37143,f479]) ).
fof(f37164,definition,
( spl54_1341
<=> rR(sK6,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_1341])],[avatar_definition]) ).
fof(f37165,plain,
( ~ rR(sK6,sK4,sK5)
| spl54_1341 ),
inference(avatar_component_clause,[],[f37164]) ).
fof(f37166,plain,
( rR(sK6,sK4,sK5)
| ~ spl54_1341 ),
inference(avatar_component_clause,[],[f37164]) ).
fof(f38885,plain,
( $false
| spl54_13
| spl54_15
| spl54_738
| spl54_1092
| ~ spl54_1277 ),
inference(forward_subsumption_resolution,[],[f36964,f21162]) ).
fof(f38886,plain,
( spl54_13
| spl54_15
| spl54_738
| spl54_1092
| ~ spl54_1277 ),
inference(avatar_contradiction_clause,[],[f38885]) ).
fof(f40372,plain,
( vd684 != sF52
| ~ spl54_730 ),
inference(superposition,[],[f1577,f20342]) ).
fof(f40915,plain,
( rR(sK5,sK5,vd1300)
| ~ rpoint(sK5)
| ~ rpoint(sK5)
| ~ rpoint(vd1300)
| ~ spl54_1090 ),
inference(resolution,[],[f26077,f979]) ).
fof(f40928,plain,
( rR(sK5,sK5,vd1300)
| ~ rpoint(sK5)
| ~ rpoint(vd1300)
| ~ spl54_1090 ),
inference(duplicate_literal_removal,[],[f40915]) ).
fof(f40935,plain,
( ~ rpoint(sK5)
| ~ rpoint(vd1300)
| ~ spl54_1090 ),
inference(forward_subsumption_resolution,[],[f40928,f1579]) ).
fof(f40939,plain,
( ~ rpoint(vd1300)
| ~ spl54_1090 ),
inference(forward_subsumption_resolution,[],[f40935,f479]) ).
fof(f40942,plain,
( $false
| ~ spl54_1090 ),
inference(forward_subsumption_resolution,[],[f40939,f547]) ).
fof(f40943,plain,
~ spl54_1090,
inference(avatar_contradiction_clause,[],[f40942]) ).
fof(f43181,plain,
( rR(sK6,sK5,sK4)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ spl54_1341 ),
inference(resolution,[],[f37166,f979]) ).
fof(f43193,plain,
( ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| spl54_1011
| ~ spl54_1341 ),
inference(forward_subsumption_resolution,[],[f43181,f24262]) ).
fof(f43200,plain,
( ~ rpoint(sK6)
| ~ rpoint(sK4)
| spl54_1011
| ~ spl54_1341 ),
inference(forward_subsumption_resolution,[],[f43193,f479]) ).
fof(f43208,plain,
( ~ rpoint(sK4)
| spl54_1011
| ~ spl54_1341 ),
inference(forward_subsumption_resolution,[],[f43200,f477]) ).
fof(f43210,plain,
( $false
| spl54_1011
| ~ spl54_1341 ),
inference(forward_subsumption_resolution,[],[f43208,f481]) ).
fof(f43211,plain,
( spl54_1011
| ~ spl54_1341 ),
inference(avatar_contradiction_clause,[],[f43210]) ).
fof(f43214,plain,
( ! [X0] :
( rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0) )
| ~ spl54_1009 ),
inference(forward_subsumption_resolution,[],[f37150,f24254]) ).
fof(f43231,plain,
( sK4 = sK5
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| vangle(sK5,sK6,sK4) = vangle(sK5,sK6,sK5)
| sK5 = sK6
| sK4 = sK6
| spl54_1011
| ~ spl54_1337 ),
inference(resolution,[],[f36624,f24262]) ).
fof(f43279,plain,
( ~ rpoint(sK5)
| ~ rpoint(sK4)
| vangle(sK5,sK6,sK4) = vangle(sK5,sK6,sK5)
| sK5 = sK6
| sK4 = sK6
| spl54_1011
| ~ spl54_1337 ),
inference(forward_subsumption_resolution,[],[f43231,f763]) ).
fof(f43294,plain,
( ~ rpoint(sK4)
| vangle(sK5,sK6,sK4) = vangle(sK5,sK6,sK5)
| sK5 = sK6
| sK4 = sK6
| spl54_1011
| ~ spl54_1337 ),
inference(forward_subsumption_resolution,[],[f43279,f479]) ).
fof(f43308,plain,
( vangle(sK5,sK6,sK4) = vangle(sK5,sK6,sK5)
| sK5 = sK6
| sK4 = sK6
| spl54_1011
| ~ spl54_1337 ),
inference(forward_subsumption_resolution,[],[f43294,f481]) ).
fof(f43322,plain,
( vangle(sK5,sK6,sK4) = vangle(sK5,sK6,sK5)
| sK4 = sK6
| spl54_1011
| ~ spl54_1337 ),
inference(forward_subsumption_resolution,[],[f43308,f788]) ).
fof(f43336,plain,
( vangle(sK5,sK6,sK4) = vangle(sK5,sK6,sK5)
| spl54_1011
| ~ spl54_1337 ),
inference(forward_subsumption_resolution,[],[f43322,f787]) ).
fof(f43349,plain,
( vd684 = vangle(sK5,sK6,sK4)
| spl54_1011
| ~ spl54_1337 ),
inference(forward_demodulation,[],[f43336,f1850]) ).
fof(f43360,plain,
( vd684 = vangle(sK4,sK6,sK5)
| spl54_1011
| ~ spl54_1337 ),
inference(forward_demodulation,[],[f43349,f2248]) ).
fof(f43426,plain,
( rR(sK5,vd1300,sK4)
| ~ rpoint(sK4)
| ~ spl54_1011 ),
inference(resolution,[],[f24261,f1758]) ).
fof(f43456,plain,
( ~ rpoint(sK4)
| ~ spl54_1011
| spl54_1075 ),
inference(forward_subsumption_resolution,[],[f43426,f24848]) ).
fof(f43457,plain,
( $false
| ~ spl54_1011
| spl54_1075 ),
inference(forward_subsumption_resolution,[],[f43456,f481]) ).
fof(f43458,plain,
( ~ spl54_1011
| spl54_1075 ),
inference(avatar_contradiction_clause,[],[f43457]) ).
fof(f43546,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0) )
| ~ spl54_1009
| spl54_1341 ),
inference(forward_subsumption_resolution,[],[f43214,f37165]) ).
fof(f43646,plain,
( spl54_1010
| ~ spl54_1009
| spl54_1341 ),
inference(avatar_split_clause,[],[f43546,f37164,f24253,f24257]) ).
fof(f43680,plain,
( ~ rline(vd1295)
| ~ ron(sK5,vd1295)
| ~ spl54_1010 ),
inference(resolution,[],[f24258,f793]) ).
fof(f43694,plain,
( ~ ron(sK5,vd1295)
| ~ spl54_1010 ),
inference(forward_subsumption_resolution,[],[f43680,f518]) ).
fof(f43701,plain,
( $false
| ~ spl54_1010 ),
inference(forward_subsumption_resolution,[],[f43694,f790]) ).
fof(f43702,plain,
~ spl54_1010,
inference(avatar_contradiction_clause,[],[f43701]) ).
fof(f43823,plain,
( $false
| spl54_738
| spl54_1011
| ~ spl54_1337 ),
inference(forward_subsumption_resolution,[],[f43360,f21162]) ).
fof(f43824,plain,
( spl54_738
| spl54_1011
| ~ spl54_1337 ),
inference(avatar_contradiction_clause,[],[f43823]) ).
fof(f43832,plain,
( vd1303 = sK6
| ~ ron(vd1303,vd1297)
| vangle(sK4,sK6,sK5) = vangle(sK5,sK6,vd1303)
| ~ spl54_1094 ),
inference(forward_subsumption_resolution,[],[f33853,f510]) ).
fof(f43899,plain,
( ~ ron(vd1303,vd1297)
| vangle(sK4,sK6,sK5) = vangle(sK5,sK6,vd1303)
| spl54_18
| ~ spl54_1094 ),
inference(forward_subsumption_resolution,[],[f43832,f1859]) ).
fof(f43937,plain,
( vangle(sK4,sK6,sK5) = vangle(sK5,sK6,vd1303)
| spl54_18
| ~ spl54_1094 ),
inference(forward_subsumption_resolution,[],[f43899,f776]) ).
fof(f43967,plain,
( vangle(sK5,sK6,sK5) = vangle(sK4,sK6,sK5)
| spl54_18
| ~ spl54_25
| ~ spl54_1094 ),
inference(forward_demodulation,[],[f43937,f2026]) ).
fof(f43996,plain,
( vd684 = vangle(sK4,sK6,sK5)
| spl54_18
| ~ spl54_25
| ~ spl54_1094 ),
inference(forward_demodulation,[],[f43967,f1850]) ).
fof(f44012,plain,
( $false
| spl54_18
| ~ spl54_25
| spl54_738
| ~ spl54_1094 ),
inference(forward_subsumption_resolution,[],[f43996,f21162]) ).
fof(f44013,plain,
( spl54_18
| ~ spl54_25
| spl54_738
| ~ spl54_1094 ),
inference(avatar_contradiction_clause,[],[f44012]) ).
fof(f44021,plain,
( spl54_1284
| ~ spl54_14 ),
inference(avatar_split_clause,[],[f1933,f1770,f29506]) ).
fof(f44043,plain,
( ~ spl54_732
| ~ spl54_730 ),
inference(avatar_split_clause,[],[f40372,f20341,f20685]) ).
cnf(s20,plain,
( ~ spl54_13
| spl54_14 ),
inference(sat_conversion,[],[f1921]) ).
cnf(s36,plain,
~ spl54_15,
inference(sat_conversion,[],[f2382]) ).
cnf(s41,plain,
~ spl54_18,
inference(sat_conversion,[],[f2583]) ).
cnf(s1060,plain,
( ~ spl54_738
| spl54_1009 ),
inference(sat_conversion,[],[f24255]) ).
cnf(s1061,plain,
( ~ spl54_738
| spl54_1010
| ~ spl54_1011 ),
inference(sat_conversion,[],[f24263]) ).
cnf(s1191,plain,
spl54_1094,
inference(sat_conversion,[],[f26282]) ).
cnf(s1192,plain,
~ spl54_1092,
inference(sat_conversion,[],[f26459]) ).
cnf(s1393,plain,
( spl54_1277
| spl54_1278 ),
inference(sat_conversion,[],[f28350]) ).
cnf(s1396,plain,
( spl54_732
| ~ spl54_1278 ),
inference(sat_conversion,[],[f28448]) ).
cnf(s1406,plain,
~ spl54_1280,
inference(sat_conversion,[],[f29818]) ).
cnf(s1441,plain,
( spl54_730
| ~ spl54_1075 ),
inference(sat_conversion,[],[f34058]) ).
cnf(s1459,plain,
( spl54_1090
| spl54_1337 ),
inference(sat_conversion,[],[f36625]) ).
cnf(s1460,plain,
( spl54_18
| spl54_25
| spl54_738
| spl54_1280
| ~ spl54_1284
| ~ spl54_1337 ),
inference(sat_conversion,[],[f36779]) ).
cnf(s1522,plain,
( spl54_13
| spl54_15
| spl54_738
| spl54_1092
| ~ spl54_1277 ),
inference(sat_conversion,[],[f38886]) ).
cnf(s1667,plain,
~ spl54_1090,
inference(sat_conversion,[],[f40943]) ).
cnf(s1834,plain,
( spl54_1011
| ~ spl54_1341 ),
inference(sat_conversion,[],[f43211]) ).
cnf(s1844,plain,
( ~ spl54_1011
| spl54_1075 ),
inference(sat_conversion,[],[f43458]) ).
cnf(s1857,plain,
( ~ spl54_1009
| spl54_1010
| spl54_1341 ),
inference(sat_conversion,[],[f43646]) ).
cnf(s1861,plain,
~ spl54_1010,
inference(sat_conversion,[],[f43702]) ).
cnf(s1879,plain,
( spl54_738
| spl54_1011
| ~ spl54_1337 ),
inference(sat_conversion,[],[f43824]) ).
cnf(s1919,plain,
( spl54_18
| ~ spl54_25
| spl54_738
| ~ spl54_1094 ),
inference(sat_conversion,[],[f44013]) ).
cnf(s1923,plain,
( ~ spl54_14
| spl54_1284 ),
inference(sat_conversion,[],[f44021]) ).
cnf(s1929,plain,
( ~ spl54_730
| ~ spl54_732 ),
inference(sat_conversion,[],[f44043]) ).
cnf(s1940,plain,
( ~ spl54_1009
| spl54_1341 ),
inference(rat,[],[s1857,s1861]) ).
cnf(s1963,plain,
spl54_1337,
inference(rat,[],[s1459,s1667]) ).
cnf(s1973,plain,
( ~ spl54_738
| ~ spl54_1011 ),
inference(rat,[],[s1061,s1861]) ).
cnf(s2084,plain,
~ spl54_738,
inference(rat,[],[s1940,s1834,s1060,s1973]) ).
cnf(s2085,plain,
spl54_1011,
inference(rat,[],[s1879,s1963,s2084]) ).
cnf(s2086,plain,
~ spl54_25,
inference(rat,[],[s1919,s1191,s41,s2084]) ).
cnf(s2087,plain,
spl54_1075,
inference(rat,[],[s1844,s2085]) ).
cnf(s2088,plain,
~ spl54_1284,
inference(rat,[],[s1460,s1963,s2084,s1406,s41,s2086]) ).
cnf(s2093,plain,
spl54_730,
inference(rat,[],[s1441,s2087]) ).
cnf(s2094,plain,
~ spl54_14,
inference(rat,[],[s1923,s2088]) ).
cnf(s2096,plain,
~ spl54_732,
inference(rat,[],[s1929,s2093]) ).
cnf(s2099,plain,
~ spl54_13,
inference(rat,[],[s20,s2094]) ).
cnf(s2103,plain,
~ spl54_1278,
inference(rat,[],[s1396,s2096]) ).
cnf(s2112,plain,
~ spl54_1277,
inference(rat,[],[s1522,s2084,s1192,s36,s2099]) ).
cnf(s2116,plain,
$false,
inference(rat,[],[s1393,s2103,s2112]) ).
fof(f44420,plain,
$false,
inference(avatar_sat_refutation,[],[s2116]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO317+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 08:07:11 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.34/2.40 % (2513279)Detected formulas, will run a generic FOF schedule.
% 10.34/2.40 % (2513286)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3057903688:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.34/2.40 % (2513287)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=779989369:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.34/2.40 % (2513284)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1478409625:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.34/2.40 % (2513289)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3359959200:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.34/2.40 % (2513285)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4027770645:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.34/2.40 % (2513288)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1987809507:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.34/2.40 % (2513290)dis-21_1_sil=8000:lcm=predicate:random_seed=2026892465:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.34/2.40 % (2513287)Instruction limit reached!
% 10.34/2.40 % (2513287)------------------------------
% 10.34/2.40 % (2513287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.34/2.40 % (2513287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.34/2.40 % (2513287)CaDiCaL version: 2.1.3
% 10.34/2.40 % (2513287)Termination reason: Instruction limit
% 10.34/2.40 % (2513287)Termination phase: Saturation
% 10.34/2.40 % (2513287)Time elapsed: 0.058 s
% 10.34/2.40 % (2513287)Peak memory usage: 89 MB
% 10.34/2.40 % (2513287)Instructions burned: 110 (million)
% 10.34/2.40 % (2513288)Instruction limit reached!
% 10.34/2.40 % (2513288)------------------------------
% 10.34/2.40 % (2513288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.34/2.40 % (2513288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.34/2.40 % (2513288)CaDiCaL version: 2.1.3
% 10.34/2.40 % (2513288)Termination reason: Instruction limit
% 10.34/2.40 % (2513288)Termination phase: Saturation
% 10.34/2.40 % (2513288)Time elapsed: 0.064 s
% 10.34/2.40 % (2513288)Peak memory usage: 89 MB
% 10.34/2.40 % (2513288)Instructions burned: 121 (million)
% 10.34/2.40 % (2513290)Instruction limit reached!
% 10.34/2.40 % (2513290)------------------------------
% 10.34/2.40 % (2513290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.34/2.40 % (2513290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.34/2.40 % (2513290)CaDiCaL version: 2.1.3
% 10.34/2.40 % (2513290)Termination reason: Instruction limit
% 10.34/2.40 % (2513290)Termination phase: Saturation
% 10.34/2.40 % (2513290)Time elapsed: 0.069 s
% 10.34/2.40 % (2513290)Peak memory usage: 90 MB
% 10.34/2.40 % (2513290)Instructions burned: 130 (million)
% 10.34/2.40 % (2513289)Instruction limit reached!
% 10.34/2.40 % (2513289)------------------------------
% 10.34/2.40 % (2513289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.34/2.40 % (2513289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.34/2.40 % (2513289)CaDiCaL version: 2.1.3
% 10.34/2.40 % (2513289)Termination reason: Instruction limit
% 10.34/2.40 % (2513289)Termination phase: Saturation
% 10.34/2.40 % (2513289)Time elapsed: 0.089 s
% 10.34/2.40 % (2513289)Peak memory usage: 90 MB
% 10.34/2.40 % (2513289)Instructions burned: 139 (million)
% 10.34/2.40 % (2513298)lrs+10_1_sil=8000:sp=occurrence:random_seed=216788067:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.34/2.40 % (2513300)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3830485535:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 10.34/2.40 % (2513299)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1674942758:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.34/2.40 % (2513301)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=4218442435:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 10.34/2.40 % (2513299)Instruction limit reached!
% 16.87/3.25 % (2513299)------------------------------
% 16.87/3.25 % (2513299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.87/3.25 % (2513299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.87/3.25 % (2513299)CaDiCaL version: 2.1.3
% 16.87/3.25 % (2513299)Termination reason: Instruction limit
% 16.87/3.25 % (2513299)Termination phase: Saturation
% 16.87/3.25 % (2513299)Time elapsed: 0.077 s
% 16.87/3.25 % (2513299)Peak memory usage: 90 MB
% 16.87/3.25 % (2513299)Instructions burned: 158 (million)
% 16.87/3.25 % (2513298)Instruction limit reached!
% 16.87/3.25 % (2513298)------------------------------
% 16.87/3.25 % (2513298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.87/3.25 % (2513298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.87/3.25 % (2513298)CaDiCaL version: 2.1.3
% 16.87/3.25 % (2513298)Termination reason: Instruction limit
% 16.87/3.25 % (2513298)Termination phase: Saturation
% 16.87/3.25 % (2513298)Time elapsed: 0.135 s
% 16.87/3.25 % (2513298)Peak memory usage: 91 MB
% 16.87/3.25 % (2513298)Instructions burned: 285 (million)
% 16.87/3.25 % (2513301)Instruction limit reached!
% 16.87/3.25 % (2513301)------------------------------
% 16.87/3.25 % (2513301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.87/3.25 % (2513301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.87/3.25 % (2513301)CaDiCaL version: 2.1.3
% 16.87/3.25 % (2513301)Termination reason: Instruction limit
% 16.87/3.25 % (2513301)Termination phase: Saturation
% 16.87/3.25 % (2513301)Time elapsed: 0.118 s
% 16.87/3.25 % (2513301)Peak memory usage: 91 MB
% 16.87/3.25 % (2513301)Instructions burned: 248 (million)
% 16.87/3.25 % (2513300)Instruction limit reached!
% 16.87/3.25 % (2513300)------------------------------
% 16.87/3.25 % (2513300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.87/3.25 % (2513300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.87/3.25 % (2513300)CaDiCaL version: 2.1.3
% 16.87/3.25 % (2513300)Termination reason: Instruction limit
% 16.87/3.25 % (2513300)Termination phase: Saturation
% 16.87/3.25 % (2513300)Time elapsed: 0.186 s
% 16.87/3.25 % (2513300)Peak memory usage: 91 MB
% 16.87/3.25 % (2513300)Instructions burned: 325 (million)
% 16.87/3.25 % (2513306)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1247646621:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 16.87/3.25 % (2513307)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=855681039:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 16.87/3.25 % (2513308)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2234388077:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 16.87/3.25 % (2513309)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2156851266:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 16.87/3.25 % (2513308)Instruction limit reached!
% 16.87/3.25 % (2513308)------------------------------
% 16.87/3.25 % (2513308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.87/3.25 % (2513308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.87/3.25 % (2513308)CaDiCaL version: 2.1.3
% 16.87/3.25 % (2513308)Termination reason: Instruction limit
% 16.87/3.25 % (2513308)Termination phase: Saturation
% 16.87/3.25 % (2513308)Time elapsed: 0.057 s
% 16.87/3.25 % (2513308)Peak memory usage: 90 MB
% 16.87/3.25 % (2513308)Instructions burned: 114 (million)
% 16.87/3.25 % (2513306)Instruction limit reached!
% 16.87/3.25 % (2513306)------------------------------
% 16.87/3.25 % (2513306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.87/3.25 % (2513306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.87/3.25 % (2513306)CaDiCaL version: 2.1.3
% 16.87/3.25 % (2513306)Termination reason: Instruction limit
% 16.87/3.25 % (2513306)Termination phase: Saturation
% 16.87/3.25 % (2513306)Time elapsed: 0.133 s
% 16.87/3.25 % (2513306)Peak memory usage: 89 MB
% 16.87/3.25 % (2513306)Instructions burned: 294 (million)
% 16.87/3.25 % (2513309)Refutation not found, incomplete strategy
% 16.87/3.25 % (2513309)------------------------------
% 16.87/3.25 % (2513309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.87/3.25 % (2513309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.87/3.25 % (2513309)CaDiCaL version: 2.1.3
% 16.87/3.25 % (2513309)Termination reason: Refutation not found, incomplete strategy
% 36.14/5.95 % (2513309)Time elapsed: 0.027 s
% 36.14/5.95 % (2513309)Peak memory usage: 89 MB
% 36.14/5.95 % (2513309)Instructions burned: 54 (million)
% 36.14/5.95 % (2513314)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2595753277:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 36.14/5.95 % (2513315)lrs+10_1_sil=8000:sp=occurrence:random_seed=2459803031:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 36.14/5.95 % (2513314)Instruction limit reached!
% 36.14/5.95 % (2513314)------------------------------
% 36.14/5.95 % (2513314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.14/5.95 % (2513314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.14/5.95 % (2513314)CaDiCaL version: 2.1.3
% 36.14/5.95 % (2513314)Termination reason: Instruction limit
% 36.14/5.95 % (2513314)Termination phase: Saturation
% 36.14/5.95 % (2513314)Time elapsed: 0.047 s
% 36.14/5.95 % (2513314)Peak memory usage: 89 MB
% 36.14/5.95 % (2513314)Instructions burned: 114 (million)
% 36.14/5.95 % (2513309)------------------------------
% 36.14/5.95 % (2513309)------------------------------
% 36.14/5.95 % (2513318)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1081695743:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 36.14/5.95 % (2513318)Refutation not found, incomplete strategy
% 36.14/5.95 % (2513318)------------------------------
% 36.14/5.95 % (2513318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.14/5.95 % (2513318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.14/5.95 % (2513318)CaDiCaL version: 2.1.3
% 36.14/5.95 % (2513318)Termination reason: Refutation not found, incomplete strategy
% 36.14/5.95 % (2513318)Time elapsed: 0.018 s
% 36.14/5.95 % (2513318)Peak memory usage: 89 MB
% 36.14/5.95 % (2513318)Instructions burned: 33 (million)
% 36.14/5.95 % (2513319)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1237016429:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 36.14/5.95 % (2513318)------------------------------
% 36.14/5.95 % (2513318)------------------------------
% 36.14/5.95 % (2513315)Instruction limit reached!
% 36.14/5.95 % (2513315)------------------------------
% 36.14/5.95 % (2513315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.14/5.95 % (2513315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.14/5.95 % (2513315)CaDiCaL version: 2.1.3
% 36.14/5.95 % (2513315)Termination reason: Instruction limit
% 36.14/5.95 % (2513315)Termination phase: Saturation
% 36.14/5.95 % (2513315)Time elapsed: 0.420 s
% 36.14/5.95 % (2513315)Peak memory usage: 95 MB
% 36.14/5.95 % (2513315)Instructions burned: 909 (million)
% 36.14/5.95 % (2513322)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4203460235:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 36.14/5.95 % (2513323)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2708744369:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 36.14/5.95 % (2513307)Instruction limit reached!
% 36.14/5.95 % (2513307)------------------------------
% 36.14/5.95 % (2513307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.14/5.95 % (2513307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.14/5.95 % (2513307)CaDiCaL version: 2.1.3
% 36.14/5.95 % (2513307)Termination reason: Instruction limit
% 36.14/5.95 % (2513307)Termination phase: Saturation
% 36.14/5.95 % (2513307)Time elapsed: 0.801 s
% 36.14/5.95 % (2513307)Peak memory usage: 142 MB
% 36.14/5.95 % (2513307)Instructions burned: 2351 (million)
% 36.14/5.95 % (2513322)Instruction limit reached!
% 36.14/5.95 % (2513322)------------------------------
% 36.14/5.95 % (2513322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.14/5.95 % (2513322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.14/5.95 % (2513322)CaDiCaL version: 2.1.3
% 36.14/5.95 % (2513322)Termination reason: Instruction limit
% 36.14/5.95 % (2513322)Termination phase: Saturation
% 36.14/5.95 % (2513322)Time elapsed: 0.066 s
% 36.14/5.95 % (2513322)Peak memory usage: 93 MB
% 36.14/5.95 % (2513322)Instructions burned: 135 (million)
% 36.14/5.95 % (2513326)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=685390234:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 36.14/5.95 % (2513327)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=616486270:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 38.27/6.24 % (2513327)Instruction limit reached!
% 38.27/6.24 % (2513327)------------------------------
% 38.27/6.24 % (2513327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.27/6.24 % (2513327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.27/6.24 % (2513327)CaDiCaL version: 2.1.3
% 38.27/6.24 % (2513327)Termination reason: Instruction limit
% 38.27/6.24 % (2513327)Termination phase: Saturation
% 38.27/6.24 % (2513327)Time elapsed: 0.066 s
% 38.27/6.24 % (2513327)Peak memory usage: 90 MB
% 38.27/6.24 % (2513327)Instructions burned: 127 (million)
% 38.27/6.24 % (2513323)Instruction limit reached!
% 38.27/6.24 % (2513323)------------------------------
% 38.27/6.24 % (2513323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.27/6.24 % (2513323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.27/6.24 % (2513323)CaDiCaL version: 2.1.3
% 38.27/6.24 % (2513323)Termination reason: Instruction limit
% 38.27/6.24 % (2513323)Termination phase: Saturation
% 38.27/6.24 % (2513323)Time elapsed: 0.298 s
% 38.27/6.24 % (2513323)Peak memory usage: 93 MB
% 38.27/6.24 % (2513323)Instructions burned: 593 (million)
% 38.27/6.24 % (2513330)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=311930541:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 38.27/6.24 % (2513331)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2110209674:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 38.27/6.24 % (2513331)Refutation not found, incomplete strategy
% 38.27/6.24 % (2513331)------------------------------
% 38.27/6.24 % (2513331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.27/6.24 % (2513331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.27/6.24 % (2513331)CaDiCaL version: 2.1.3
% 38.27/6.24 % (2513331)Termination reason: Refutation not found, incomplete strategy
% 38.27/6.24 % (2513331)Time elapsed: 0.013 s
% 38.27/6.24 % (2513331)Peak memory usage: 89 MB
% 38.27/6.24 % (2513331)Instructions burned: 26 (million)
% 38.27/6.24 % (2513330)Instruction limit reached!
% 38.27/6.24 % (2513330)------------------------------
% 38.27/6.24 % (2513330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.27/6.24 % (2513330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.27/6.24 % (2513330)CaDiCaL version: 2.1.3
% 38.27/6.24 % (2513330)Termination reason: Instruction limit
% 38.27/6.24 % (2513330)Termination phase: Saturation
% 38.27/6.24 % (2513330)Time elapsed: 0.077 s
% 38.27/6.24 % (2513330)Peak memory usage: 91 MB
% 38.27/6.24 % (2513330)Instructions burned: 135 (million)
% 38.27/6.24 % (2513334)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2787707419:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 38.27/6.24 % (2513334)Refutation not found, incomplete strategy
% 38.27/6.24 % (2513334)------------------------------
% 38.27/6.24 % (2513334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.27/6.24 % (2513334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.27/6.24 % (2513334)CaDiCaL version: 2.1.3
% 38.27/6.24 % (2513334)Termination reason: Refutation not found, incomplete strategy
% 38.27/6.24 % (2513334)Time elapsed: 0.007 s
% 38.27/6.24 % (2513334)Peak memory usage: 89 MB
% 38.27/6.24 % (2513334)Instructions burned: 11 (million)
% 38.27/6.24 % (2513331)------------------------------
% 38.27/6.24 % (2513331)------------------------------
% 38.27/6.24 % (2513336)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3838960662:i=6060:aac=none:ins=25_2979 on theBenchmark for (2979ds/6060Mi)
% 38.27/6.24 % (2513334)------------------------------
% 38.27/6.24 % (2513334)------------------------------
% 38.27/6.24 % (2513338)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1518127516:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2977 on theBenchmark for (2977ds/150Mi)
% 38.27/6.24 % (2513338)Instruction limit reached!
% 38.27/6.24 % (2513338)------------------------------
% 38.27/6.24 % (2513338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.27/6.24 % (2513338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.27/6.24 % (2513338)CaDiCaL version: 2.1.3
% 38.27/6.24 % (2513338)Termination reason: Instruction limit
% 38.27/6.24 % (2513338)Termination phase: Saturation
% 38.27/6.24 % (2513338)Time elapsed: 0.076 s
% 38.27/6.24 % (2513338)Peak memory usage: 92 MB
% 38.27/6.24 % (2513338)Instructions burned: 151 (million)
% 38.27/6.24 % (2513340)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=356910828:i=14155:bd=all_2975 on theBenchmark for (2975ds/14155Mi)
% 38.27/6.24 % (2513319)Instruction limit reached!
% 38.27/6.24 % (2513319)------------------------------
% 38.27/6.24 % (2513319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.27/6.24 % (2513319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.27/6.24 % (2513319)CaDiCaL version: 2.1.3
% 38.27/6.24 % (2513319)Termination reason: Instruction limit
% 38.27/6.24 % (2513319)Termination phase: Saturation
% 38.27/6.24 % (2513319)Time elapsed: 2.692 s
% 38.27/6.24 % (2513319)Peak memory usage: 142 MB
% 38.27/6.24 % (2513319)Instructions burned: 5204 (million)
% 38.27/6.24 % (2513342)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2013232427:i=667:av=off:fsr=off_2962 on theBenchmark for (2962ds/667Mi)
% 38.27/6.24 % (2513342)Refutation not found, incomplete strategy
% 38.27/6.24 % (2513342)------------------------------
% 38.27/6.24 % (2513342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.27/6.24 % (2513342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.27/6.24 % (2513342)CaDiCaL version: 2.1.3
% 38.27/6.24 % (2513342)Termination reason: Refutation not found, incomplete strategy
% 38.27/6.24 % (2513342)Time elapsed: 0.022 s
% 38.27/6.24 % (2513342)Peak memory usage: 89 MB
% 38.27/6.24 % (2513342)Instructions burned: 45 (million)
% 38.27/6.24 % (2513342)------------------------------
% 38.27/6.24 % (2513342)------------------------------
% 38.27/6.24 % (2513344)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1710916316:s2a=on:i=185:s2at=1.8:fdi=4_2958 on theBenchmark for (2958ds/185Mi)
% 38.27/6.24 % (2513344)Instruction limit reached!
% 38.27/6.24 % (2513344)------------------------------
% 38.27/6.24 % (2513344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.27/6.24 % (2513344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.27/6.24 % (2513344)CaDiCaL version: 2.1.3
% 38.27/6.24 % (2513344)Termination reason: Instruction limit
% 38.27/6.24 % (2513344)Termination phase: Saturation
% 38.27/6.24 % (2513344)Time elapsed: 0.095 s
% 38.27/6.24 % (2513344)Peak memory usage: 93 MB
% 38.27/6.24 % (2513344)Instructions burned: 185 (million)
% 38.27/6.24 % (2513346)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1006628672:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2956 on theBenchmark for (2956ds/193Mi)
% 38.27/6.24 % (2513346)Instruction limit reached!
% 38.27/6.24 % (2513346)------------------------------
% 38.27/6.24 % (2513346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.27/6.24 % (2513346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.27/6.24 % (2513346)CaDiCaL version: 2.1.3
% 38.27/6.24 % (2513346)Termination reason: Instruction limit
% 38.27/6.24 % (2513346)Termination phase: Saturation
% 38.27/6.24 % (2513346)Time elapsed: 0.105 s
% 38.27/6.24 % (2513346)Peak memory usage: 91 MB
% 38.27/6.24 % (2513346)Instructions burned: 194 (million)
% 38.27/6.24 % (2513348)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4181336196:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2953 on theBenchmark for (2953ds/4850Mi)
% 38.27/6.24 % (2513348)Refutation not found, incomplete strategy
% 38.27/6.24 % (2513348)------------------------------
% 38.27/6.24 % (2513348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.27/6.24 % (2513348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.27/6.24 % (2513348)CaDiCaL version: 2.1.3
% 38.27/6.24 % (2513348)Termination reason: Refutation not found, incomplete strategy
% 38.27/6.24 % (2513348)Time elapsed: 0.017 s
% 38.27/6.24 % (2513348)Peak memory usage: 89 MB
% 38.27/6.24 % (2513348)Instructions burned: 32 (million)
% 38.27/6.24 % (2513348)------------------------------
% 38.27/6.24 % (2513348)------------------------------
% 38.27/6.24 % (2513284)First to succeed.
% 38.27/6.24 % (2513284)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2513279"
% 38.27/6.24 % (2513350)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3561631429:i=12111:sd=1:ss=included_2949 on theBenchmark for (2949ds/12111Mi)
% 38.27/6.24 % (2513284)Refutation found. Thanks to Tanya!
% 38.27/6.24 % SZS status Theorem for theBenchmark
% 38.27/6.24 % SZS output start Proof for theBenchmark
% See solution above
% 38.63/6.34 % (2513284)------------------------------
% 38.63/6.34 % (2513284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.63/6.34 % (2513284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/6.34 % (2513284)CaDiCaL version: 2.1.3
% 38.63/6.34 % (2513284)Termination reason: Refutation
% 38.63/6.34 % (2513284)Time elapsed: 4.976 s
% 38.63/6.34 % (2513284)Peak memory usage: 171 MB
% 38.63/6.34 % (2513284)Instructions burned: 8644 (million)
% 38.63/6.34 % (2513284)------------------------------
% 38.63/6.34 % (2513284)------------------------------
% 38.63/6.34 % (2513279)Success in time 5.398 s
% 38.63/6.34 % Vampire exiting
%------------------------------------------------------------------------------