%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO316+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:25 AM UTC 2026
% Result : Theorem 34.64s 6.02s
% Output : Refutation 36.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 84
% Syntax : Number of formulae : 849 ( 154 unt; 40 def)
% Number of atoms : 4624 (1357 equ)
% Maximal formula atoms : 26 ( 5 avg)
% Number of connectives : 6692 (2917 ~;3521 |; 195 &)
% ( 42 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 46 ( 44 usr; 37 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 19 con; 0-3 aty)
% Number of variables : 1388 ( 0 sgn1333 !; 55 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vplus(vangle(vd1288,vd1289,vd1299),vangle(vd1287,vd1289,vd1288)) = vangle(vd1287,vd1289,vd1299),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(363, 1326, 0)') ).
fof(f2,negated_conjecture,
vplus(vangle(vd1288,vd1289,vd1299),vangle(vd1287,vd1289,vd1288)) != vangle(vd1287,vd1289,vd1299),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
vangle(vd1288,vd1289,vd1299) = vangle(vd1289,vd1288,vd1306),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct2(362), 1325, 0)') ).
fof(f4,axiom,
vangle(vd1299,vd1288,vd1289) = vangle(vd1306,vd1289,vd1288),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct1(362), 1324, 0)') ).
fof(f5,axiom,
vf(vd1288,vd1299) = vf(vd1289,vd1306),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(361, 1323, 0)') ).
fof(f8,axiom,
vf(vd1299,vd1289) = vf(vd1288,vd1306),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct1(360), 1321, 0)') ).
fof(f13,axiom,
vf(vd1299,vd1289) = vf(vd1306,vd1288),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct1(359), 1318, 0)') ).
fof(f14,axiom,
rpoint(vd1306),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(352, 0)') ).
fof(f15,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/sandbox/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(f16,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/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))') ).
fof(f17,axiom,
! [X0,X1] :
( ( ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> vf(X0,X1) = vf(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(166), 0), imp(cond(axiom(166), 0)))') ).
fof(f20,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/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(188), 0), imp(cond(axiom(188), 0)))') ).
fof(f27,axiom,
~ rR(vd1287,vd1289,vd1306),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','neg(neg(conjunct2(356)))') ).
fof(f33,axiom,
~ rR(vd1287,vd1288,vd1299),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','neg(neg(356))') ).
fof(f35,axiom,
( vd1302 = vd1303
& rR(vd1289,vd1287,vd1302)
& rpoint(vd1303)
& rR(vd1288,vd1287,vd1299) ),
file('/export/starexec/sandbox/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(f38,axiom,
rline(vd1297),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(347, 0)') ).
fof(f41,axiom,
rline(vd1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(346, 0)') ).
fof(f46,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/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(168), 0), imp(cond(axiom(168), 0)))') ).
fof(f48,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/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(89), 0), imp(cond(axiom(89), 0)))') ).
fof(f49,axiom,
! [X0,X1,X2,X3,X4] :
( ( X3 = X4
& ron(X1,X3)
& ron(X0,X3)
& rR(X1,X0,X2)
& rline(X4)
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ron(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(83), 0), imp(cond(axiom(83), 0)))') ).
fof(f50,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/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))') ).
fof(f53,axiom,
vd1289 != vd1287,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(355)), 1313, 0)') ).
fof(f54,axiom,
vd1288 != vd1287,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct1(355), 1312, 0)') ).
fof(f55,axiom,
ron(vd1289,vd1297),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(354))))), 0)') ).
fof(f56,axiom,
ron(vd1288,vd1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(354))))), 0)') ).
fof(f58,axiom,
ron(vd1287,vd1297),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(conjunct2(354))), 0)') ).
fof(f59,axiom,
ron(vd1299,vd1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(354)), 0)') ).
fof(f60,axiom,
ron(vd1287,vd1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(conjunct1(354), 0)') ).
fof(f61,axiom,
vd1299 != vd1287,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct2(conjunct2(conjunct2(353))), 1311, 0)') ).
fof(f63,axiom,
vd1306 != vd1287,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(353)), 1309, 0)') ).
fof(f64,axiom,
ron(vd1306,vd1297),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(conjunct1(353), 0)') ).
fof(f65,axiom,
vd1299 = vd1300,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(348, 4)') ).
fof(f66,axiom,
rpoint(vd1300),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(348, 1)') ).
fof(f68,axiom,
! [X0,X1] :
( ( ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ( vf(X0,X1) = v0
<=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))') ).
fof(f69,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/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(51), 0), imp(cond(axiom(51), 0)))') ).
fof(f78,axiom,
! [X0,X1,X2,X3,X4] :
( ( X3 = X4
& ron(X2,X3)
& ron(X0,X3)
& rR(X1,X0,X2)
& rline(X4)
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ron(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(85), 0), imp(cond(axiom(85), 0)))') ).
fof(f79,axiom,
! [X0,X1,X2,X3] :
( ( ron(X1,X3)
& ron(X1,X2)
& ron(X0,X3)
& ron(X0,X2)
& ? [X4] :
( X3 = X4
& rline(X4) )
& ? [X5] :
( X2 = X5
& rline(X5) )
& X0 != X1
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> X2 = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(73), 0), imp(cond(axiom(73), 0)))') ).
fof(f80,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/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))') ).
fof(f83,axiom,
! [X0,X1] :
( ( X0 = X1
& rreal(X1) )
=> vplus(X0,v0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(141), 0), imp(cond(axiom(141), 0)))') ).
fof(f84,axiom,
v0 = vd684,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(axiom(137), 2)') ).
fof(f85,axiom,
rreal(vd684),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(axiom(137), 1)') ).
fof(f91,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/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(53), 0), imp(cond(axiom(53), 0)))') ).
fof(f105,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/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(119), 0), imp(cond(axiom(119), 0)))') ).
fof(f115,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/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(93), 0), imp(cond(axiom(93), 0)))') ).
fof(f117,axiom,
! [X0,X1] :
( rcenter(X0,X1)
=> rinside(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))') ).
fof(f158,plain,
vplus(vangle(vd1288,vd1289,vd1299),vangle(vd1287,vd1289,vd1288)) != vangle(vd1287,vd1289,vd1299),
inference(flattening,[],[f2]) ).
fof(f171,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,[],[f16]) ).
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(flattening,[],[f171]) ).
fof(f173,plain,
! [X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f17]) ).
fof(f174,plain,
! [X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f173]) ).
fof(f175,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,[],[f20]) ).
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(flattening,[],[f175]) ).
fof(f197,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,[],[f46]) ).
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(flattening,[],[f197]) ).
fof(f201,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,[],[f48]) ).
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(flattening,[],[f201]) ).
fof(f203,plain,
! [X0,X1,X2,X3,X4] :
( ron(X2,X3)
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f49]) ).
fof(f204,plain,
! [X0,X1,X2,X3,X4] :
( ron(X2,X3)
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f203]) ).
fof(f205,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,[],[f50]) ).
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(flattening,[],[f205]) ).
fof(f209,plain,
! [X0,X1] :
( ( vf(X0,X1) = v0
<=> X0 = X1 )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f68]) ).
fof(f210,plain,
! [X0,X1] :
( ( vf(X0,X1) = v0
<=> X0 = X1 )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f209]) ).
fof(f211,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,[],[f69]) ).
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(flattening,[],[f211]) ).
fof(f227,plain,
! [X0,X1,X2,X3,X4] :
( ron(X1,X3)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f78]) ).
fof(f228,plain,
! [X0,X1,X2,X3,X4] :
( ron(X1,X3)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f227]) ).
fof(f229,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ ron(X1,X3)
| ~ ron(X1,X2)
| ~ ron(X0,X3)
| ~ ron(X0,X2)
| ! [X4] :
( X3 != X4
| ~ rline(X4) )
| ! [X5] :
( X2 != X5
| ~ rline(X5) )
| X0 = X1
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f79]) ).
fof(f230,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ ron(X1,X3)
| ~ ron(X1,X2)
| ~ ron(X0,X3)
| ~ ron(X0,X2)
| ! [X4] :
( X3 != X4
| ~ rline(X4) )
| ! [X5] :
( X2 != X5
| ~ rline(X5) )
| X0 = X1
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f229]) ).
fof(f231,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,[],[f80]) ).
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(flattening,[],[f231]) ).
fof(f237,plain,
! [X0,X1] :
( vplus(X0,v0) = X0
| X0 != X1
| ~ rreal(X1) ),
inference(ennf_transformation,[],[f83]) ).
fof(f238,plain,
! [X0,X1] :
( vplus(X0,v0) = X0
| X0 != X1
| ~ rreal(X1) ),
inference(flattening,[],[f237]) ).
fof(f249,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,[],[f91]) ).
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(flattening,[],[f249]) ).
fof(f276,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,[],[f105]) ).
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(flattening,[],[f276]) ).
fof(f296,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,[],[f115]) ).
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(flattening,[],[f296]) ).
fof(f300,plain,
! [X0,X1] :
( rinside(X0,X1)
| ~ rcenter(X0,X1) ),
inference(ennf_transformation,[],[f117]) ).
fof(f380,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)],[f15]) ).
fof(f381,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,[],[f176]) ).
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(flattening,[],[f381]) ).
fof(f388,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,[],[f210]) ).
fof(f389,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,[],[f212]) ).
fof(f390,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))],[f389]) ).
fof(f400,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,[],[f250]) ).
fof(f401,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))],[f400]) ).
fof(f451,plain,
vplus(vangle(vd1288,vd1289,vd1299),vangle(vd1287,vd1289,vd1288)) != vangle(vd1287,vd1289,vd1299),
inference(cnf_transformation,[],[f158]) ).
fof(f452,plain,
vangle(vd1288,vd1289,vd1299) = vangle(vd1289,vd1288,vd1306),
inference(cnf_transformation,[],[f3]) ).
fof(f453,plain,
vangle(vd1299,vd1288,vd1289) = vangle(vd1306,vd1289,vd1288),
inference(cnf_transformation,[],[f4]) ).
fof(f454,plain,
vf(vd1288,vd1299) = vf(vd1289,vd1306),
inference(cnf_transformation,[],[f5]) ).
fof(f459,plain,
vf(vd1299,vd1289) = vf(vd1288,vd1306),
inference(cnf_transformation,[],[f8]) ).
fof(f473,plain,
vf(vd1299,vd1289) = vf(vd1306,vd1288),
inference(cnf_transformation,[],[f13]) ).
fof(f474,plain,
rpoint(vd1306),
inference(cnf_transformation,[],[f14]) ).
fof(f475,plain,
rpoint(sK6),
inference(cnf_transformation,[],[f380]) ).
fof(f476,plain,
vd1287 = sK6,
inference(cnf_transformation,[],[f380]) ).
fof(f477,plain,
rpoint(sK5),
inference(cnf_transformation,[],[f380]) ).
fof(f478,plain,
vd1288 = sK5,
inference(cnf_transformation,[],[f380]) ).
fof(f479,plain,
rpoint(sK4),
inference(cnf_transformation,[],[f380]) ).
fof(f480,plain,
vd1289 = sK4,
inference(cnf_transformation,[],[f380]) ).
fof(f483,plain,
vd1288 != vd1289,
inference(cnf_transformation,[],[f380]) ).
fof(f484,plain,
vf(vd1287,vd1288) = vf(vd1287,vd1289),
inference(cnf_transformation,[],[f380]) ).
fof(f485,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,[],[f172]) ).
fof(f486,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f174]) ).
fof(f489,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,[],[f382]) ).
fof(f490,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,[],[f382]) ).
fof(f491,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,[],[f382]) ).
fof(f498,plain,
~ rR(vd1287,vd1289,vd1306),
inference(cnf_transformation,[],[f27]) ).
fof(f505,plain,
~ rR(vd1287,vd1288,vd1299),
inference(cnf_transformation,[],[f33]) ).
fof(f507,plain,
rR(vd1288,vd1287,vd1299),
inference(cnf_transformation,[],[f35]) ).
fof(f508,plain,
rpoint(vd1303),
inference(cnf_transformation,[],[f35]) ).
fof(f509,plain,
rR(vd1289,vd1287,vd1302),
inference(cnf_transformation,[],[f35]) ).
fof(f510,plain,
vd1302 = vd1303,
inference(cnf_transformation,[],[f35]) ).
fof(f513,plain,
rline(vd1297),
inference(cnf_transformation,[],[f38]) ).
fof(f516,plain,
rline(vd1295),
inference(cnf_transformation,[],[f41]) ).
fof(f522,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,[],[f198]) ).
fof(f524,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,[],[f202]) ).
fof(f525,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X2,X3)
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f204]) ).
fof(f526,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,[],[f206]) ).
fof(f528,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,[],[f206]) ).
fof(f529,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,[],[f206]) ).
fof(f532,plain,
vd1289 != vd1287,
inference(cnf_transformation,[],[f53]) ).
fof(f533,plain,
vd1288 != vd1287,
inference(cnf_transformation,[],[f54]) ).
fof(f534,plain,
ron(vd1289,vd1297),
inference(cnf_transformation,[],[f55]) ).
fof(f535,plain,
ron(vd1288,vd1295),
inference(cnf_transformation,[],[f56]) ).
fof(f537,plain,
ron(vd1287,vd1297),
inference(cnf_transformation,[],[f58]) ).
fof(f538,plain,
ron(vd1299,vd1295),
inference(cnf_transformation,[],[f59]) ).
fof(f539,plain,
ron(vd1287,vd1295),
inference(cnf_transformation,[],[f60]) ).
fof(f540,plain,
vd1299 != vd1287,
inference(cnf_transformation,[],[f61]) ).
fof(f542,plain,
vd1287 != vd1306,
inference(cnf_transformation,[],[f63]) ).
fof(f543,plain,
ron(vd1306,vd1297),
inference(cnf_transformation,[],[f64]) ).
fof(f544,plain,
vd1299 = vd1300,
inference(cnf_transformation,[],[f65]) ).
fof(f545,plain,
rpoint(vd1300),
inference(cnf_transformation,[],[f66]) ).
fof(f548,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| vf(X0,X1) != v0
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f388]) ).
fof(f549,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = v0
| X0 != X1
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f388]) ).
fof(f550,plain,
! [X3,X0,X1,X4] :
( rline(sK7(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f390]) ).
fof(f551,plain,
! [X3,X0,X1,X4] :
( ron(X0,sK7(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f390]) ).
fof(f552,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK7(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f390]) ).
fof(f576,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X1,X3)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f228]) ).
fof(f577,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( X2 = X3
| ~ ron(X1,X3)
| ~ ron(X1,X2)
| ~ ron(X0,X3)
| ~ ron(X0,X2)
| X3 != X4
| ~ rline(X4)
| X2 != X5
| ~ rline(X5)
| X0 = X1
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f230]) ).
fof(f578,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,[],[f232]) ).
fof(f581,plain,
! [X0,X1] :
( vplus(X0,v0) = X0
| X0 != X1
| ~ rreal(X1) ),
inference(cnf_transformation,[],[f238]) ).
fof(f582,plain,
v0 = vd684,
inference(cnf_transformation,[],[f84]) ).
fof(f583,plain,
rreal(vd684),
inference(cnf_transformation,[],[f85]) ).
fof(f599,plain,
! [X3,X0,X1,X4] :
( rcircle(sK15(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f401]) ).
fof(f600,plain,
! [X3,X0,X1,X4] :
( rcenter(X0,sK15(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f401]) ).
fof(f601,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK15(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f401]) ).
fof(f629,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,[],[f277]) ).
fof(f639,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,[],[f297]) ).
fof(f641,plain,
! [X0,X1] :
( ~ rcenter(X0,X1)
| rinside(X0,X1) ),
inference(cnf_transformation,[],[f300]) ).
fof(f751,plain,
vplus(vangle(sK5,sK4,vd1300),vangle(sK6,sK4,sK5)) != vangle(sK6,sK4,vd1300),
inference(definition_unfolding,[],[f451,f478,f480,f544,f476,f480,f478,f476,f480,f544]) ).
fof(f752,plain,
vangle(sK5,sK4,vd1300) = vangle(sK4,sK5,vd1306),
inference(definition_unfolding,[],[f452,f478,f480,f544,f480,f478]) ).
fof(f753,plain,
vangle(vd1300,sK5,sK4) = vangle(vd1306,sK4,sK5),
inference(definition_unfolding,[],[f453,f544,f478,f480,f480,f478]) ).
fof(f754,plain,
vf(sK5,vd1300) = vf(sK4,vd1306),
inference(definition_unfolding,[],[f454,f478,f544,f480]) ).
fof(f756,plain,
vf(vd1300,sK4) = vf(sK5,vd1306),
inference(definition_unfolding,[],[f459,f544,f480,f478]) ).
fof(f758,plain,
vf(vd1300,sK4) = vf(vd1306,sK5),
inference(definition_unfolding,[],[f473,f544,f480,f478]) ).
fof(f759,plain,
vf(sK6,sK5) = vf(sK6,sK4),
inference(definition_unfolding,[],[f484,f476,f478,f476,f480]) ).
fof(f760,plain,
sK4 != sK5,
inference(definition_unfolding,[],[f483,f478,f480]) ).
fof(f765,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,[],[f491,f582]) ).
fof(f766,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,[],[f490,f582]) ).
fof(f767,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,[],[f489,f582]) ).
fof(f771,plain,
~ rR(sK6,sK4,vd1306),
inference(definition_unfolding,[],[f498,f476,f480]) ).
fof(f774,plain,
~ rR(sK6,sK5,vd1300),
inference(definition_unfolding,[],[f505,f476,f478,f544]) ).
fof(f776,plain,
rR(sK4,sK6,vd1303),
inference(definition_unfolding,[],[f509,f480,f476,f510]) ).
fof(f777,plain,
rR(sK5,sK6,vd1300),
inference(definition_unfolding,[],[f507,f478,f476,f544]) ).
fof(f784,plain,
sK4 != sK6,
inference(definition_unfolding,[],[f532,f480,f476]) ).
fof(f785,plain,
sK5 != sK6,
inference(definition_unfolding,[],[f533,f478,f476]) ).
fof(f786,plain,
ron(sK4,vd1297),
inference(definition_unfolding,[],[f534,f480]) ).
fof(f787,plain,
ron(sK5,vd1295),
inference(definition_unfolding,[],[f535,f478]) ).
fof(f788,plain,
ron(sK6,vd1297),
inference(definition_unfolding,[],[f537,f476]) ).
fof(f789,plain,
ron(vd1300,vd1295),
inference(definition_unfolding,[],[f538,f544]) ).
fof(f790,plain,
ron(sK6,vd1295),
inference(definition_unfolding,[],[f539,f476]) ).
fof(f791,plain,
vd1300 != sK6,
inference(definition_unfolding,[],[f540,f544,f476]) ).
fof(f793,plain,
vd1306 != sK6,
inference(definition_unfolding,[],[f542,f476]) ).
fof(f794,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = vd684
| X0 != X1
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(definition_unfolding,[],[f549,f582]) ).
fof(f795,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| vf(X0,X1) != vd684
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(definition_unfolding,[],[f548,f582]) ).
fof(f796,plain,
! [X0,X1] :
( vplus(X0,vd684) = X0
| X0 != X1
| ~ rreal(X1) ),
inference(definition_unfolding,[],[f581,f582]) ).
fof(f890,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,[],[f485]) ).
fof(f891,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,[],[f890]) ).
fof(f892,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,[],[f891]) ).
fof(f893,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,[],[f892]) ).
fof(f894,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,[],[f893]) ).
fof(f895,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,[],[f894]) ).
fof(f896,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,[],[f895]) ).
fof(f897,plain,
! [X2,X3,X0] :
( vf(X0,X2) = vf(X2,X0)
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f486]) ).
fof(f898,plain,
! [X2,X3] :
( ~ rpoint(X3)
| ~ rpoint(X2)
| vf(X3,X2) = vf(X2,X3) ),
inference(equality_resolution,[],[f897]) ).
fof(f899,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,[],[f765]) ).
fof(f900,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,[],[f899]) ).
fof(f901,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,[],[f900]) ).
fof(f902,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,[],[f901]) ).
fof(f903,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,[],[f766]) ).
fof(f904,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,[],[f903]) ).
fof(f905,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,[],[f904]) ).
fof(f906,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,[],[f905]) ).
fof(f907,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,[],[f767]) ).
fof(f908,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,[],[f907]) ).
fof(f909,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,[],[f908]) ).
fof(f910,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,[],[f909]) ).
fof(f949,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,[],[f522]) ).
fof(f950,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,[],[f949]) ).
fof(f951,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,[],[f950]) ).
fof(f955,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,[],[f524]) ).
fof(f956,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,[],[f955]) ).
fof(f957,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,[],[f956]) ).
fof(f958,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,[],[f957]) ).
fof(f959,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ron(X2,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f525]) ).
fof(f960,plain,
! [X0,X1,X6,X7,X4,X5] :
( ron(X5,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rR(X1,X0,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f959]) ).
fof(f961,plain,
! [X0,X6,X7,X4,X5] :
( ron(X5,X4)
| ~ ron(X6,X4)
| ~ ron(X0,X4)
| ~ rR(X6,X0,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f960]) ).
fof(f962,plain,
! [X6,X7,X4,X5] :
( ~ rR(X6,X7,X5)
| ~ ron(X6,X4)
| ~ ron(X7,X4)
| ron(X5,X4)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f961]) ).
fof(f963,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,[],[f529]) ).
fof(f964,plain,
! [X3,X0,X4,X5] :
( ~ rR(X0,X4,X3)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f963]) ).
fof(f965,plain,
! [X3,X4,X5] :
( ~ rR(X5,X4,X3)
| ~ rR(X4,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f964]) ).
fof(f966,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,[],[f528]) ).
fof(f967,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X3,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f966]) ).
fof(f968,plain,
! [X3,X4,X5] :
( ~ rR(X4,X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f967]) ).
fof(f969,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f968]) ).
fof(f974,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,[],[f526]) ).
fof(f975,plain,
! [X3,X0,X4,X5] :
( rR(X4,X3,X0)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f974]) ).
fof(f976,plain,
! [X3,X4,X5] :
( ~ rR(X4,X5,X3)
| rR(X4,X3,X5)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f975]) ).
fof(f981,plain,
! [X2,X3,X1] :
( vd684 = vf(X1,X1)
| X1 != X2
| ~ rpoint(X2)
| X1 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f794]) ).
fof(f982,plain,
! [X2,X3] :
( vd684 = vf(X2,X2)
| ~ rpoint(X2)
| X2 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f981]) ).
fof(f983,plain,
! [X3] :
( vd684 = vf(X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f982]) ).
fof(f984,plain,
! [X2,X3,X0] :
( X0 = X2
| vf(X0,X2) != vd684
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f795]) ).
fof(f985,plain,
! [X2,X3] :
( vd684 != vf(X3,X2)
| X2 = X3
| ~ rpoint(X2)
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f984]) ).
fof(f986,plain,
! [X3,X0,X4] :
( ron(X3,sK7(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f552]) ).
fof(f987,plain,
! [X3,X4] :
( ron(X3,sK7(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f986]) ).
fof(f988,plain,
! [X3,X0,X4] :
( ron(X0,sK7(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f551]) ).
fof(f989,plain,
! [X3,X4] :
( ron(X4,sK7(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f988]) ).
fof(f990,plain,
! [X3,X0,X4] :
( rline(sK7(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f550]) ).
fof(f991,plain,
! [X3,X4] :
( rline(sK7(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f990]) ).
fof(f1044,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ron(X1,X4)
| ~ ron(X2,X4)
| ~ ron(X0,X4)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f576]) ).
fof(f1045,plain,
! [X0,X1,X6,X7,X4,X5] :
( ron(X1,X4)
| ~ ron(X5,X4)
| ~ ron(X0,X4)
| ~ rR(X1,X0,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1044]) ).
fof(f1046,plain,
! [X0,X6,X7,X4,X5] :
( ron(X6,X4)
| ~ ron(X5,X4)
| ~ ron(X0,X4)
| ~ rR(X6,X0,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1045]) ).
fof(f1047,plain,
! [X6,X7,X4,X5] :
( ~ rR(X6,X7,X5)
| ~ ron(X5,X4)
| ~ ron(X7,X4)
| ron(X6,X4)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1046]) ).
fof(f1048,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( X2 = X4
| ~ ron(X1,X4)
| ~ ron(X1,X2)
| ~ ron(X0,X4)
| ~ ron(X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rline(X5)
| X0 = X1
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f577]) ).
fof(f1049,plain,
! [X0,X1,X6,X7,X4,X5] :
( X4 = X5
| ~ ron(X1,X4)
| ~ ron(X1,X5)
| ~ ron(X0,X4)
| ~ ron(X0,X5)
| ~ rline(X4)
| ~ rline(X5)
| X0 = X1
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1048]) ).
fof(f1050,plain,
! [X0,X6,X7,X4,X5] :
( X4 = X5
| ~ ron(X6,X4)
| ~ ron(X6,X5)
| ~ ron(X0,X4)
| ~ ron(X0,X5)
| ~ rline(X4)
| ~ rline(X5)
| X0 = X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1049]) ).
fof(f1051,plain,
! [X6,X7,X4,X5] :
( ~ ron(X7,X5)
| ~ ron(X6,X4)
| ~ ron(X6,X5)
| ~ ron(X7,X4)
| X4 = X5
| ~ rline(X4)
| ~ rline(X5)
| X6 = X7
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1050]) ).
fof(f1052,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,[],[f578]) ).
fof(f1053,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,[],[f1052]) ).
fof(f1059,plain,
! [X1] :
( ~ rreal(X1)
| vplus(X1,vd684) = X1 ),
inference(equality_resolution,[],[f796]) ).
fof(f1102,plain,
! [X3,X0,X4] :
( ron(X3,sK15(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f601]) ).
fof(f1103,plain,
! [X3,X4] :
( ron(X3,sK15(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1102]) ).
fof(f1104,plain,
! [X3,X0,X4] :
( rcenter(X0,sK15(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f600]) ).
fof(f1105,plain,
! [X3,X4] :
( rcenter(X4,sK15(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1104]) ).
fof(f1106,plain,
! [X3,X0,X4] :
( rcircle(sK15(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f599]) ).
fof(f1107,plain,
! [X3,X4] :
( rcircle(sK15(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1106]) ).
fof(f1197,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,[],[f629]) ).
fof(f1198,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,[],[f1197]) ).
fof(f1199,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,[],[f1198]) ).
fof(f1200,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,[],[f1199]) ).
fof(f1201,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,[],[f1200]) ).
fof(f1246,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,[],[f639]) ).
fof(f1247,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,[],[f1246]) ).
fof(f1248,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,[],[f1247]) ).
fof(f1249,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,[],[f1248]) ).
fof(f1570,definition,
sF52 = vangle(sK5,sK4,vd1300),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f1571,plain,
vangle(sK5,sK4,vd1300) = sF52,
inference(reorient_equations,[],[f1570]) ).
fof(f1572,definition,
sF53 = vangle(sK6,sK4,sK5),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f1573,plain,
vangle(sK6,sK4,sK5) = sF53,
inference(reorient_equations,[],[f1572]) ).
fof(f1574,definition,
sF54 = vplus(sF52,sF53),
introduced(definition,[new_symbols(definition,[sF54])],[function_definition]) ).
fof(f1575,plain,
vplus(sF52,sF53) = sF54,
inference(reorient_equations,[],[f1574]) ).
fof(f1576,definition,
sF55 = vangle(sK6,sK4,vd1300),
introduced(definition,[new_symbols(definition,[sF55])],[function_definition]) ).
fof(f1577,plain,
vangle(sK6,sK4,vd1300) = sF55,
inference(reorient_equations,[],[f1576]) ).
fof(f1578,plain,
sF54 != sF55,
inference(definition_folding,[],[f751,f1577,f1575,f1573,f1571]) ).
fof(f1579,plain,
! [X3] :
( ~ rpoint(X3)
| vd684 = vf(X3,X3) ),
inference(duplicate_literal_removal,[],[f983]) ).
fof(f1581,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f969]) ).
fof(f1629,plain,
vangle(sK4,sK5,vd1306) = sF52,
inference(forward_demodulation,[],[f1571,f752]) ).
fof(f1630,plain,
( rR(sK5,vd1300,sK6)
| ~ rpoint(vd1300)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(resolution,[],[f976,f777]) ).
fof(f1631,plain,
( rR(sK4,vd1303,sK6)
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(resolution,[],[f976,f776]) ).
fof(f1632,plain,
( rR(sK4,vd1303,sK6)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1631,f508]) ).
fof(f1633,plain,
( rR(sK5,vd1300,sK6)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1630,f545]) ).
fof(f1634,plain,
( rR(sK4,vd1303,sK6)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1632,f479]) ).
fof(f1635,plain,
( rR(sK5,vd1300,sK6)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1633,f477]) ).
fof(f1636,plain,
rR(sK4,vd1303,sK6),
inference(forward_subsumption_resolution,[],[f1634,f475]) ).
fof(f1637,plain,
rR(sK5,vd1300,sK6),
inference(forward_subsumption_resolution,[],[f1635,f475]) ).
fof(f1668,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,[],[f896,f790]) ).
fof(f1670,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,[],[f896,f786]) ).
fof(f1671,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,[],[f896,f788]) ).
fof(f1688,plain,
( ~ rR(vd1300,sK5,sK6)
| ~ rpoint(sK6)
| ~ rpoint(vd1300)
| ~ rpoint(sK5) ),
inference(resolution,[],[f965,f1637]) ).
fof(f1693,plain,
( ~ rR(vd1300,sK5,sK6)
| ~ rpoint(vd1300)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f1688,f475]) ).
fof(f1698,plain,
( ~ rR(vd1300,sK5,sK6)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f1693,f545]) ).
fof(f1703,plain,
~ rR(vd1300,sK5,sK6),
inference(forward_subsumption_resolution,[],[f1698,f477]) ).
fof(f1710,plain,
vd684 = vf(sK4,sK4),
inference(resolution,[],[f1579,f479]) ).
fof(f1713,plain,
! [X0,X1] :
( rR(X0,X1,sK5)
| vd684 = vangle(X1,X0,sK5)
| ~ ron(X1,vd1295)
| ~ ron(X0,vd1295)
| sK5 = X0
| X0 = X1
| ~ rline(vd1295)
| ~ rpoint(sK5)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f910,f787]) ).
fof(f1716,plain,
! [X0,X1] :
( rR(X0,X1,vd1306)
| vd684 = vangle(X1,X0,vd1306)
| ~ ron(X1,vd1297)
| ~ ron(X0,vd1297)
| vd1306 = X0
| X0 = X1
| ~ rline(vd1297)
| ~ rpoint(vd1306)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f910,f543]) ).
fof(f1730,plain,
! [X0] :
( ~ rpoint(X0)
| vf(vd1300,X0) = vf(X0,vd1300) ),
inference(resolution,[],[f898,f545]) ).
fof(f1763,plain,
! [X0] :
( ~ rR(sK6,sK5,X0)
| rR(sK5,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(vd1300) ),
inference(resolution,[],[f958,f1637]) ).
fof(f1764,plain,
! [X0] :
( ~ rR(sK6,sK4,X0)
| rR(sK4,vd1303,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) ),
inference(resolution,[],[f958,f1636]) ).
fof(f1767,plain,
! [X0] :
( ~ rR(sK6,sK4,X0)
| rR(sK4,vd1303,X0)
| ~ rpoint(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) ),
inference(forward_subsumption_resolution,[],[f1764,f475]) ).
fof(f1768,plain,
! [X0] :
( ~ rR(sK6,sK5,X0)
| rR(sK5,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f1763,f475]) ).
fof(f1773,plain,
! [X0] :
( ~ rR(sK6,sK4,X0)
| rR(sK4,vd1303,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1303) ),
inference(forward_subsumption_resolution,[],[f1767,f479]) ).
fof(f1774,plain,
! [X0] :
( ~ rR(sK6,sK5,X0)
| rR(sK5,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f1768,f477]) ).
fof(f1779,plain,
! [X0] :
( ~ rR(sK6,sK4,X0)
| rR(sK4,vd1303,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1773,f508]) ).
fof(f1780,plain,
! [X0] :
( ~ rR(sK6,sK5,X0)
| rR(sK5,vd1300,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1774,f545]) ).
fof(f1788,definition,
( spl56_13
<=> vd1300 = sK4 ),
introduced(definition,[new_symbols(definition,[spl56_13])],[avatar_definition]) ).
fof(f1789,plain,
( vd1300 != sK4
| spl56_13 ),
inference(avatar_component_clause,[],[f1788]) ).
fof(f1790,plain,
( vd1300 = sK4
| ~ spl56_13 ),
inference(avatar_component_clause,[],[f1788]) ).
fof(f1800,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK4 = X1
| ~ rpoint(X0)
| sK4 = X0
| vangle(X0,X1,sK4) = vangle(sK4,X1,X0) ),
inference(resolution,[],[f951,f479]) ).
fof(f1801,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK5 = X1
| ~ rpoint(X0)
| sK5 = X0
| vangle(X0,X1,sK5) = vangle(sK5,X1,X0) ),
inference(resolution,[],[f951,f477]) ).
fof(f1803,plain,
( vd684 != vf(sK4,vd1306)
| vd1300 = sK5
| ~ rpoint(vd1300)
| ~ rpoint(sK5) ),
inference(superposition,[],[f985,f754]) ).
fof(f1804,plain,
( vd684 != vf(sK4,vd1306)
| vd1300 = sK5
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f1803,f545]) ).
fof(f1805,plain,
( vd684 != vf(sK4,vd1306)
| vd1300 = sK5 ),
inference(forward_subsumption_resolution,[],[f1804,f477]) ).
fof(f1807,definition,
( spl56_15
<=> vd1300 = sK5 ),
introduced(definition,[new_symbols(definition,[spl56_15])],[avatar_definition]) ).
fof(f1808,plain,
( vd1300 != sK5
| spl56_15 ),
inference(avatar_component_clause,[],[f1807]) ).
fof(f1809,plain,
( vd1300 = sK5
| ~ spl56_15 ),
inference(avatar_component_clause,[],[f1807]) ).
fof(f1811,definition,
( spl56_16
<=> vd684 = vf(sK4,vd1306) ),
introduced(definition,[new_symbols(definition,[spl56_16])],[avatar_definition]) ).
fof(f1813,plain,
( vd684 != vf(sK4,vd1306)
| spl56_16 ),
inference(avatar_component_clause,[],[f1811]) ).
fof(f1814,plain,
( spl56_15
| ~ spl56_16 ),
inference(avatar_split_clause,[],[f1805,f1811,f1807]) ).
fof(f1820,plain,
! [X0] :
( vd684 != sF53
| ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK4,X0)
| sK4 = sK5
| sK4 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK4) ),
inference(superposition,[],[f906,f1573]) ).
fof(f1875,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X2,X3)
| ~ ron(X2,sK7(X1,X0))
| ~ ron(X0,X3)
| sK7(X1,X0) = X3
| ~ rline(X3)
| ~ rline(sK7(X1,X0))
| X0 = X2
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f987,f1051]) ).
fof(f1876,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,[],[f987,f910]) ).
fof(f1879,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,[],[f1876]) ).
fof(f1880,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X2,X3)
| ~ ron(X2,sK7(X1,X0))
| ~ ron(X0,X3)
| sK7(X1,X0) = X3
| ~ rline(X3)
| ~ rline(sK7(X1,X0))
| X0 = X2
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f1875]) ).
fof(f1882,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,[],[f1879,f991]) ).
fof(f1883,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,sK7(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X2,X3)
| X0 = X1
| ~ ron(X0,X3)
| sK7(X1,X0) = X3
| ~ rline(X3)
| X0 = X2
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f1880,f991]) ).
fof(f1884,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,[],[f1882,f987]) ).
fof(f1885,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,[],[f1884]) ).
fof(f1886,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,[],[f1885,f1581]) ).
fof(f1889,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,[],[f989,f1886]) ).
fof(f1891,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X2,X3)
| ~ ron(X2,sK7(X1,X0))
| ~ ron(X1,X3)
| sK7(X1,X0) = X3
| ~ rline(X3)
| ~ rline(sK7(X1,X0))
| X1 = X2
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(resolution,[],[f989,f1051]) ).
fof(f1893,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,[],[f989,f896]) ).
fof(f1894,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,[],[f1893]) ).
fof(f1896,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X2,X3)
| ~ ron(X2,sK7(X1,X0))
| ~ ron(X1,X3)
| sK7(X1,X0) = X3
| ~ rline(X3)
| ~ rline(sK7(X1,X0))
| X1 = X2
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f1891]) ).
fof(f1898,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X1
| vd684 = vangle(X0,X1,X0) ),
inference(duplicate_literal_removal,[],[f1889]) ).
fof(f1899,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,[],[f1894,f991]) ).
fof(f1901,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,sK7(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X2,X3)
| X0 = X1
| ~ ron(X1,X3)
| sK7(X1,X0) = X3
| ~ rline(X3)
| X1 = X2
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f1896,f991]) ).
fof(f1905,plain,
! [X0] :
( ~ rpoint(X0)
| sK4 = X0
| vd684 = vangle(X0,sK4,X0) ),
inference(resolution,[],[f1898,f479]) ).
fof(f1907,plain,
! [X0] :
( ~ rpoint(X0)
| sK6 = X0
| vd684 = vangle(X0,sK6,X0) ),
inference(resolution,[],[f1898,f475]) ).
fof(f1932,plain,
( vd684 != vf(vd1300,sK4)
| vd1306 = sK5
| ~ rpoint(sK5)
| ~ rpoint(vd1306) ),
inference(superposition,[],[f985,f758]) ).
fof(f1933,plain,
( vd684 != vf(vd1300,sK4)
| vd1306 = sK5
| ~ rpoint(vd1306) ),
inference(forward_subsumption_resolution,[],[f1932,f477]) ).
fof(f1934,plain,
( vd684 != vf(vd1300,sK4)
| vd1306 = sK5 ),
inference(forward_subsumption_resolution,[],[f1933,f474]) ).
fof(f1935,plain,
( vd684 != vf(sK5,vd1306)
| vd1306 = sK5 ),
inference(forward_demodulation,[],[f1934,f756]) ).
fof(f1939,plain,
vf(vd1300,sK4) = vf(sK4,vd1300),
inference(resolution,[],[f1730,f479]) ).
fof(f1943,plain,
vf(sK5,vd1306) = vf(sK4,vd1300),
inference(forward_demodulation,[],[f1939,f756]) ).
fof(f1968,plain,
! [X0] :
( ~ rR(sK4,vd1303,X0)
| ~ rR(sK4,sK6,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) ),
inference(resolution,[],[f1249,f1636]) ).
fof(f1971,plain,
! [X0] :
( ~ rR(sK4,vd1303,X0)
| ~ rR(sK4,sK6,X0)
| ~ rpoint(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) ),
inference(forward_subsumption_resolution,[],[f1968,f475]) ).
fof(f1977,plain,
! [X0] :
( ~ rR(sK4,vd1303,X0)
| ~ rR(sK4,sK6,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1303) ),
inference(forward_subsumption_resolution,[],[f1971,f479]) ).
fof(f1983,plain,
! [X0] :
( ~ rR(sK4,sK6,X0)
| ~ rR(sK4,vd1303,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1977,f508]) ).
fof(f2010,plain,
( sK4 = sK5
| vd684 = vangle(sK5,sK4,sK5) ),
inference(resolution,[],[f1905,f477]) ).
fof(f2011,plain,
( sK4 = sK6
| vd684 = vangle(sK6,sK4,sK6) ),
inference(resolution,[],[f1905,f475]) ).
fof(f2012,plain,
vd684 = vangle(sK6,sK4,sK6),
inference(forward_subsumption_resolution,[],[f2011,f784]) ).
fof(f2013,plain,
vd684 = vangle(sK5,sK4,sK5),
inference(forward_subsumption_resolution,[],[f2010,f760]) ).
fof(f2033,definition,
( spl56_30
<=> vd1306 = sK4 ),
introduced(definition,[new_symbols(definition,[spl56_30])],[avatar_definition]) ).
fof(f2034,plain,
( vd1306 != sK4
| spl56_30 ),
inference(avatar_component_clause,[],[f2033]) ).
fof(f2035,plain,
( vd1306 = sK4
| ~ spl56_30 ),
inference(avatar_component_clause,[],[f2033]) ).
fof(f2061,plain,
( vd684 != vf(sK4,vd1300)
| vd1306 = sK5 ),
inference(forward_demodulation,[],[f1935,f1943]) ).
fof(f2065,plain,
( vd684 != vf(sK4,sK4)
| vd1306 = sK5
| ~ spl56_13 ),
inference(forward_demodulation,[],[f2061,f1790]) ).
fof(f2068,plain,
( vd1306 = sK5
| ~ spl56_13 ),
inference(forward_subsumption_resolution,[],[f2065,f1710]) ).
fof(f2214,plain,
( vd1300 = sK6
| vd684 = vangle(vd1300,sK6,vd1300) ),
inference(resolution,[],[f1907,f545]) ).
fof(f2215,plain,
( sK4 = sK6
| vd684 = vangle(sK4,sK6,sK4) ),
inference(resolution,[],[f1907,f479]) ).
fof(f2216,plain,
( sK5 = sK6
| vd684 = vangle(sK5,sK6,sK5) ),
inference(resolution,[],[f1907,f477]) ).
fof(f2218,plain,
vd684 = vangle(sK5,sK6,sK5),
inference(forward_subsumption_resolution,[],[f2216,f785]) ).
fof(f2219,plain,
vd684 = vangle(sK4,sK6,sK4),
inference(forward_subsumption_resolution,[],[f2215,f784]) ).
fof(f2220,plain,
vd684 = vangle(vd1300,sK6,vd1300),
inference(forward_subsumption_resolution,[],[f2214,f791]) ).
fof(f2315,plain,
! [X0] :
( sK4 = sK5
| ~ rpoint(X0)
| sK4 = X0
| vangle(X0,sK5,sK4) = vangle(sK4,sK5,X0) ),
inference(resolution,[],[f1800,f477]) ).
fof(f2316,plain,
! [X0] :
( sK4 = sK6
| ~ rpoint(X0)
| sK4 = X0
| vangle(X0,sK6,sK4) = vangle(sK4,sK6,X0) ),
inference(resolution,[],[f1800,f475]) ).
fof(f2317,plain,
! [X0] :
( ~ rpoint(X0)
| sK4 = X0
| vangle(X0,sK6,sK4) = vangle(sK4,sK6,X0) ),
inference(forward_subsumption_resolution,[],[f2316,f784]) ).
fof(f2318,plain,
! [X0] :
( ~ rpoint(X0)
| sK4 = X0
| vangle(X0,sK5,sK4) = vangle(sK4,sK5,X0) ),
inference(forward_subsumption_resolution,[],[f2315,f760]) ).
fof(f2362,plain,
( vd1300 = sK4
| vangle(vd1300,sK5,sK4) = vangle(sK4,sK5,vd1300) ),
inference(resolution,[],[f2318,f545]) ).
fof(f2374,plain,
( vd1306 = sK4
| vangle(vd1306,sK6,sK4) = vangle(sK4,sK6,vd1306) ),
inference(resolution,[],[f2317,f474]) ).
fof(f2422,plain,
! [X0] :
( sK4 = sK5
| ~ rpoint(X0)
| sK5 = X0
| vangle(X0,sK4,sK5) = vangle(sK5,sK4,X0) ),
inference(resolution,[],[f1801,f479]) ).
fof(f2426,plain,
! [X0] :
( ~ rpoint(X0)
| sK5 = X0
| vangle(X0,sK4,sK5) = vangle(sK5,sK4,X0) ),
inference(forward_subsumption_resolution,[],[f2422,f760]) ).
fof(f2489,definition,
( spl56_39
<=> vd1306 = sK5 ),
introduced(definition,[new_symbols(definition,[spl56_39])],[avatar_definition]) ).
fof(f2490,plain,
( vd1306 != sK5
| spl56_39 ),
inference(avatar_component_clause,[],[f2489]) ).
fof(f2491,plain,
( vd1306 = sK5
| ~ spl56_39 ),
inference(avatar_component_clause,[],[f2489]) ).
fof(f2502,definition,
( spl56_41
<=> vangle(vd1306,sK6,sK4) = vangle(sK4,sK6,vd1306) ),
introduced(definition,[new_symbols(definition,[spl56_41])],[avatar_definition]) ).
fof(f2504,plain,
( vangle(vd1306,sK6,sK4) = vangle(sK4,sK6,vd1306)
| ~ spl56_41 ),
inference(avatar_component_clause,[],[f2502]) ).
fof(f2505,plain,
( spl56_41
| spl56_30 ),
inference(avatar_split_clause,[],[f2374,f2033,f2502]) ).
fof(f2565,plain,
( rR(sK5,sK5,sK6)
| ~ spl56_15 ),
inference(superposition,[],[f1637,f1809]) ).
fof(f2567,plain,
( ~ rR(sK5,sK5,sK6)
| ~ spl56_15 ),
inference(superposition,[],[f1703,f1809]) ).
fof(f2576,plain,
( $false
| ~ spl56_15 ),
inference(forward_subsumption_resolution,[],[f2565,f2567]) ).
fof(f2577,plain,
~ spl56_15,
inference(avatar_contradiction_clause,[],[f2576]) ).
fof(f2611,plain,
( vd684 != vf(sK4,sK4)
| spl56_16
| ~ spl56_30 ),
inference(superposition,[],[f1813,f2035]) ).
fof(f2614,plain,
( $false
| spl56_16
| ~ spl56_30 ),
inference(forward_subsumption_resolution,[],[f2611,f1710]) ).
fof(f2615,plain,
( spl56_16
| ~ spl56_30 ),
inference(avatar_contradiction_clause,[],[f2614]) ).
fof(f2641,plain,
( vd1306 = sK5
| vangle(vd1306,sK4,sK5) = vangle(sK5,sK4,vd1306) ),
inference(resolution,[],[f2426,f474]) ).
fof(f2647,plain,
( sK5 = sK6
| vangle(sK6,sK4,sK5) = vangle(sK5,sK4,sK6) ),
inference(resolution,[],[f2426,f475]) ).
fof(f2648,plain,
vangle(sK6,sK4,sK5) = vangle(sK5,sK4,sK6),
inference(forward_subsumption_resolution,[],[f2647,f785]) ).
fof(f2653,plain,
sF53 = vangle(sK5,sK4,sK6),
inference(forward_demodulation,[],[f2648,f1573]) ).
fof(f2658,plain,
! [X0] :
( vd684 != sF53
| ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| sK4 = sK6
| sK4 = sK5
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(sK4) ),
inference(superposition,[],[f906,f2653]) ).
fof(f2871,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,[],[f1053,f759]) ).
fof(f2878,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,[],[f2871,f477]) ).
fof(f3876,plain,
! [X0,X1] :
( rinside(X0,sK15(X0,X1))
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f641,f1105]) ).
fof(f3877,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,[],[f3876,f1201]) ).
fof(f3878,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,[],[f3877]) ).
fof(f3879,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,[],[f3878,f1107]) ).
fof(f6570,plain,
! [X0,X1] :
( X0 = X1
| ~ ron(sK4,X1)
| ~ ron(sK5,X0)
| ~ rcenter(sK6,X1)
| ~ rcenter(sK6,X0)
| ~ rpoint(sK4) ),
inference(equality_resolution,[],[f2878]) ).
fof(f6575,plain,
! [X0,X1] :
( ~ rcenter(sK6,X1)
| ~ ron(sK4,X1)
| ~ ron(sK5,X0)
| X0 = X1
| ~ rcenter(sK6,X0) ),
inference(forward_subsumption_resolution,[],[f6570,f479]) ).
fof(f6584,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,[],[f6575,f1105]) ).
fof(f6585,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,[],[f6584,f475]) ).
fof(f6606,plain,
! [X0] :
( ~ ron(sK5,X0)
| sK15(sK6,sK4) = X0
| ~ rcenter(sK6,X0)
| sK4 = sK6
| ~ rpoint(sK4)
| sK4 = sK6
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(resolution,[],[f6585,f1103]) ).
fof(f6607,plain,
! [X0] :
( ~ ron(sK5,X0)
| sK15(sK6,sK4) = X0
| ~ rcenter(sK6,X0)
| sK4 = sK6
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(duplicate_literal_removal,[],[f6606]) ).
fof(f6608,plain,
! [X0] :
( ~ ron(sK5,X0)
| sK15(sK6,sK4) = X0
| ~ rcenter(sK6,X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f6607,f784]) ).
fof(f6609,plain,
! [X0] :
( ~ ron(sK5,X0)
| sK15(sK6,sK4) = X0
| ~ rcenter(sK6,X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f6608,f479]) ).
fof(f6610,plain,
! [X0] :
( ~ rcenter(sK6,X0)
| sK15(sK6,sK4) = X0
| ~ ron(sK5,X0) ),
inference(forward_subsumption_resolution,[],[f6609,f475]) ).
fof(f6611,plain,
! [X0] :
( sK15(sK6,X0) = sK15(sK6,sK4)
| ~ ron(sK5,sK15(sK6,X0))
| sK6 = X0
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(resolution,[],[f6610,f1105]) ).
fof(f6612,plain,
! [X0] :
( ~ ron(sK5,sK15(sK6,X0))
| sK15(sK6,X0) = sK15(sK6,sK4)
| sK6 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f6611,f475]) ).
fof(f6613,plain,
( sK15(sK6,sK4) = sK15(sK6,sK5)
| sK5 = sK6
| ~ rpoint(sK5)
| sK5 = sK6
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(resolution,[],[f6612,f1103]) ).
fof(f6614,plain,
( sK15(sK6,sK4) = sK15(sK6,sK5)
| sK5 = sK6
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(duplicate_literal_removal,[],[f6613]) ).
fof(f6615,plain,
( sK15(sK6,sK4) = sK15(sK6,sK5)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f6614,f785]) ).
fof(f6616,plain,
( sK15(sK6,sK4) = sK15(sK6,sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f6615,f477]) ).
fof(f6617,plain,
sK15(sK6,sK4) = sK15(sK6,sK5),
inference(forward_subsumption_resolution,[],[f6616,f475]) ).
fof(f6622,plain,
( ron(sK5,sK15(sK6,sK4))
| sK5 = sK6
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(superposition,[],[f1103,f6617]) ).
fof(f6623,plain,
( ron(sK5,sK15(sK6,sK4))
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f6622,f785]) ).
fof(f6627,plain,
( ron(sK5,sK15(sK6,sK4))
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f6623,f477]) ).
fof(f6631,plain,
ron(sK5,sK15(sK6,sK4)),
inference(forward_subsumption_resolution,[],[f6627,f475]) ).
fof(f7032,plain,
( ! [X0] :
( vd684 != vangle(sK4,sK6,vd1306)
| ~ rR(sK6,vd1306,sK4)
| ~ ron(vd1306,X0)
| ~ ron(sK6,X0)
| sK4 = sK6
| vd1306 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1306)
| ~ rpoint(sK6) )
| ~ spl56_41 ),
inference(superposition,[],[f902,f2504]) ).
fof(f12346,plain,
vd684 = vplus(vd684,vd684),
inference(resolution,[],[f583,f1059]) ).
fof(f14900,plain,
( spl56_39
| ~ spl56_13 ),
inference(avatar_split_clause,[],[f2068,f1788,f2489]) ).
fof(f15067,plain,
( vangle(vd1306,sK4,sK5) = vangle(sK5,sK4,vd1306)
| spl56_39 ),
inference(forward_subsumption_resolution,[],[f2641,f2490]) ).
fof(f15103,plain,
( vangle(vd1300,sK5,sK4) = vangle(sK4,sK5,vd1300)
| spl56_13 ),
inference(forward_subsumption_resolution,[],[f2362,f1789]) ).
fof(f15688,plain,
( vangle(vd1300,sK5,sK4) = vangle(sK5,sK4,vd1306)
| spl56_39 ),
inference(forward_demodulation,[],[f15067,f753]) ).
fof(f15713,plain,
( vangle(sK4,sK5,vd1300) = vangle(sK5,sK4,vd1306)
| spl56_13
| spl56_39 ),
inference(forward_demodulation,[],[f15688,f15103]) ).
fof(f15827,plain,
( ! [X0] :
( vd684 != vangle(sK4,sK5,vd1300)
| ~ rR(sK5,vd1300,sK4)
| ~ ron(vd1300,X0)
| ~ ron(sK5,X0)
| sK4 = sK5
| vd1300 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1300)
| ~ rpoint(sK5) )
| spl56_13 ),
inference(superposition,[],[f902,f15103]) ).
fof(f23167,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,[],[f1671,f513]) ).
fof(f23168,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,[],[f1670,f513]) ).
fof(f23170,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,[],[f1668,f516]) ).
fof(f23180,plain,
! [X0,X1] :
( rR(X0,X1,vd1306)
| vd684 = vangle(X1,X0,vd1306)
| ~ ron(X1,vd1297)
| ~ ron(X0,vd1297)
| vd1306 = X0
| X0 = X1
| ~ rpoint(vd1306)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1716,f513]) ).
fof(f23183,plain,
! [X0,X1] :
( rR(X0,X1,sK5)
| vd684 = vangle(X1,X0,sK5)
| ~ ron(X1,vd1295)
| ~ ron(X0,vd1295)
| sK5 = X0
| X0 = X1
| ~ rpoint(sK5)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1713,f516]) ).
fof(f23196,plain,
! [X0] :
( vd684 != sF53
| ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK4,X0)
| sK4 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f1820,f760]) ).
fof(f23234,plain,
! [X0] :
( vd684 != sF53
| ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| sK4 = sK5
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f2658,f784]) ).
fof(f23378,plain,
( ! [X0] :
( vd684 != vangle(sK4,sK6,vd1306)
| ~ rR(sK6,vd1306,sK4)
| ~ ron(vd1306,X0)
| ~ ron(sK6,X0)
| vd1306 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1306)
| ~ rpoint(sK6) )
| ~ spl56_41 ),
inference(forward_subsumption_resolution,[],[f7032,f784]) ).
fof(f23477,plain,
( ! [X0] :
( vd684 != vangle(sK4,sK5,vd1300)
| ~ rR(sK5,vd1300,sK4)
| ~ ron(vd1300,X0)
| ~ ron(sK5,X0)
| vd1300 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1300)
| ~ rpoint(sK5) )
| spl56_13 ),
inference(forward_subsumption_resolution,[],[f15827,f760]) ).
fof(f23535,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,[],[f23167,f475]) ).
fof(f23536,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,[],[f23168,f479]) ).
fof(f23538,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,[],[f23170,f475]) ).
fof(f23548,plain,
! [X0,X1] :
( rR(X0,X1,vd1306)
| vd684 = vangle(X1,X0,vd1306)
| ~ ron(X1,vd1297)
| ~ ron(X0,vd1297)
| vd1306 = X0
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f23180,f474]) ).
fof(f23551,plain,
! [X0,X1] :
( rR(X0,X1,sK5)
| vd684 = vangle(X1,X0,sK5)
| ~ ron(X1,vd1295)
| ~ ron(X0,vd1295)
| sK5 = X0
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f23183,f477]) ).
fof(f23564,plain,
! [X0] :
( vd684 != sF53
| ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f23196,f784]) ).
fof(f23600,plain,
! [X0] :
( vd684 != sF53
| ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f23234,f760]) ).
fof(f23772,plain,
( ! [X0] :
( vd684 != vangle(sK4,sK6,vd1306)
| ~ rR(sK6,vd1306,sK4)
| ~ ron(vd1306,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1306)
| ~ rpoint(sK6) )
| ~ spl56_41 ),
inference(forward_subsumption_resolution,[],[f23378,f793]) ).
fof(f23885,plain,
( ! [X0] :
( vd684 != vangle(sK4,sK5,vd1300)
| ~ rR(sK5,vd1300,sK4)
| ~ ron(vd1300,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1300)
| ~ rpoint(sK5) )
| spl56_13
| spl56_15 ),
inference(forward_subsumption_resolution,[],[f23477,f1808]) ).
fof(f23952,plain,
! [X0] :
( vd684 != sF53
| ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f23564,f477]) ).
fof(f23981,plain,
! [X0] :
( vd684 != sF53
| ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f23600,f475]) ).
fof(f24116,plain,
( ! [X0] :
( vd684 != vangle(sK4,sK6,vd1306)
| ~ rR(sK6,vd1306,sK4)
| ~ ron(vd1306,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(vd1306)
| ~ rpoint(sK6) )
| ~ spl56_41 ),
inference(forward_subsumption_resolution,[],[f23772,f479]) ).
fof(f24169,plain,
( ! [X0] :
( vd684 != vangle(sK4,sK5,vd1300)
| ~ rR(sK5,vd1300,sK4)
| ~ ron(vd1300,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(vd1300)
| ~ rpoint(sK5) )
| spl56_13
| spl56_15 ),
inference(forward_subsumption_resolution,[],[f23885,f479]) ).
fof(f24210,plain,
! [X0] :
( vd684 != sF53
| ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f23952,f475]) ).
fof(f24227,plain,
! [X0] :
( vd684 != sF53
| ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f23981,f477]) ).
fof(f24342,plain,
( ! [X0] :
( vd684 != vangle(sK4,sK6,vd1306)
| ~ rR(sK6,vd1306,sK4)
| ~ ron(vd1306,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK6) )
| ~ spl56_41 ),
inference(forward_subsumption_resolution,[],[f24116,f474]) ).
fof(f24383,plain,
( ! [X0] :
( vd684 != vangle(sK4,sK5,vd1300)
| ~ rR(sK5,vd1300,sK4)
| ~ ron(vd1300,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| spl56_13
| spl56_15 ),
inference(forward_subsumption_resolution,[],[f24169,f545]) ).
fof(f24417,plain,
! [X0] :
( vd684 != sF53
| ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK4,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f24210,f479]) ).
fof(f24434,plain,
! [X0] :
( vd684 != sF53
| ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f24227,f479]) ).
fof(f24481,plain,
( ! [X0] :
( vd684 != vangle(sK4,sK6,vd1306)
| ~ rR(sK6,vd1306,sK4)
| ~ ron(vd1306,X0)
| ~ ron(sK6,X0)
| ~ rline(X0) )
| ~ spl56_41 ),
inference(forward_subsumption_resolution,[],[f24342,f475]) ).
fof(f24501,plain,
( ! [X0] :
( vd684 != vangle(sK4,sK5,vd1300)
| ~ rR(sK5,vd1300,sK4)
| ~ ron(vd1300,X0)
| ~ ron(sK5,X0)
| ~ rline(X0) )
| spl56_13
| spl56_15 ),
inference(forward_subsumption_resolution,[],[f24383,f477]) ).
fof(f24514,definition,
( spl56_1278
<=> ! [X0] :
( ~ ron(sK4,X0)
| ~ rline(X0)
| ~ ron(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl56_1278])],[avatar_definition]) ).
fof(f24515,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ rline(X0)
| ~ ron(sK4,X0) )
| ~ spl56_1278 ),
inference(avatar_component_clause,[],[f24514]) ).
fof(f24517,definition,
( spl56_1279
<=> rR(sK5,sK4,vd1306) ),
introduced(definition,[new_symbols(definition,[spl56_1279])],[avatar_definition]) ).
fof(f24518,plain,
( rR(sK5,sK4,vd1306)
| ~ spl56_1279 ),
inference(avatar_component_clause,[],[f24517]) ).
fof(f24519,plain,
( ~ rR(sK5,sK4,vd1306)
| spl56_1279 ),
inference(avatar_component_clause,[],[f24517]) ).
fof(f24521,definition,
( spl56_1280
<=> vd684 = sF52 ),
introduced(definition,[new_symbols(definition,[spl56_1280])],[avatar_definition]) ).
fof(f24522,plain,
( vd684 = sF52
| ~ spl56_1280 ),
inference(avatar_component_clause,[],[f24521]) ).
fof(f24523,plain,
( vd684 != sF52
| spl56_1280 ),
inference(avatar_component_clause,[],[f24521]) ).
fof(f24526,definition,
( spl56_1281
<=> ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl56_1281])],[avatar_definition]) ).
fof(f24527,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(sK4,X0) )
| ~ spl56_1281 ),
inference(avatar_component_clause,[],[f24526]) ).
fof(f24529,definition,
( spl56_1282
<=> rR(sK4,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl56_1282])],[avatar_definition]) ).
fof(f24530,plain,
( rR(sK4,sK6,sK5)
| ~ spl56_1282 ),
inference(avatar_component_clause,[],[f24529]) ).
fof(f24531,plain,
( ~ rR(sK4,sK6,sK5)
| spl56_1282 ),
inference(avatar_component_clause,[],[f24529]) ).
fof(f24533,definition,
( spl56_1283
<=> vd684 = sF53 ),
introduced(definition,[new_symbols(definition,[spl56_1283])],[avatar_definition]) ).
fof(f24534,plain,
( vd684 = sF53
| ~ spl56_1283 ),
inference(avatar_component_clause,[],[f24533]) ).
fof(f24538,definition,
( spl56_1284
<=> rR(sK4,sK6,vd1300) ),
introduced(definition,[new_symbols(definition,[spl56_1284])],[avatar_definition]) ).
fof(f24539,plain,
( rR(sK4,sK6,vd1300)
| ~ spl56_1284 ),
inference(avatar_component_clause,[],[f24538]) ).
fof(f24540,plain,
( ~ rR(sK4,sK6,vd1300)
| spl56_1284 ),
inference(avatar_component_clause,[],[f24538]) ).
fof(f24542,definition,
( spl56_1285
<=> vd684 = sF55 ),
introduced(definition,[new_symbols(definition,[spl56_1285])],[avatar_definition]) ).
fof(f24543,plain,
( vd684 = sF55
| ~ spl56_1285 ),
inference(avatar_component_clause,[],[f24542]) ).
fof(f24552,definition,
( spl56_1286
<=> ! [X0] :
( ron(sK5,X0)
| ~ rline(X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0) ) ),
introduced(definition,[new_symbols(definition,[spl56_1286])],[avatar_definition]) ).
fof(f24553,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(sK4,X0)
| ron(sK5,X0) )
| ~ spl56_1286 ),
inference(avatar_component_clause,[],[f24552]) ).
fof(f24554,plain,
( spl56_1286
| ~ spl56_1283 ),
inference(avatar_split_clause,[],[f24417,f24533,f24552]) ).
fof(f24569,definition,
( spl56_1289
<=> ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(vd1306,X0) ) ),
introduced(definition,[new_symbols(definition,[spl56_1289])],[avatar_definition]) ).
fof(f24570,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(vd1306,X0) )
| ~ spl56_1289 ),
inference(avatar_component_clause,[],[f24569]) ).
fof(f24596,definition,
( spl56_1295
<=> ! [X0] :
( ron(sK6,X0)
| ~ rline(X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl56_1295])],[avatar_definition]) ).
fof(f24597,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ rline(X0)
| ron(sK6,X0)
| ~ ron(sK4,X0) )
| ~ spl56_1295 ),
inference(avatar_component_clause,[],[f24596]) ).
fof(f24616,plain,
( spl56_1295
| ~ spl56_1283 ),
inference(avatar_split_clause,[],[f24434,f24533,f24596]) ).
fof(f24618,definition,
( spl56_1300
<=> ! [X0] :
( ~ ron(vd1300,X0)
| ~ rline(X0)
| ~ ron(sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl56_1300])],[avatar_definition]) ).
fof(f24619,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ rline(X0)
| ~ ron(vd1300,X0) )
| ~ spl56_1300 ),
inference(avatar_component_clause,[],[f24618]) ).
fof(f24626,definition,
( spl56_1302
<=> ! [X0] :
( ron(sK5,X0)
| ~ rline(X0)
| ~ ron(sK4,X0)
| ~ ron(vd1300,X0) ) ),
introduced(definition,[new_symbols(definition,[spl56_1302])],[avatar_definition]) ).
fof(f24627,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ rline(X0)
| ron(sK5,X0)
| ~ ron(vd1300,X0) )
| ~ spl56_1302 ),
inference(avatar_component_clause,[],[f24626]) ).
fof(f24630,definition,
( spl56_1303
<=> ! [X0] :
( ~ ron(sK5,X0)
| ~ rline(X0)
| ~ ron(sK6,X0) ) ),
introduced(definition,[new_symbols(definition,[spl56_1303])],[avatar_definition]) ).
fof(f24631,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(sK5,X0) )
| ~ spl56_1303 ),
inference(avatar_component_clause,[],[f24630]) ).
fof(f24633,definition,
( spl56_1304
<=> rR(sK6,sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl56_1304])],[avatar_definition]) ).
fof(f24634,plain,
( rR(sK6,sK5,sK4)
| ~ spl56_1304 ),
inference(avatar_component_clause,[],[f24633]) ).
fof(f24635,plain,
( ~ rR(sK6,sK5,sK4)
| spl56_1304 ),
inference(avatar_component_clause,[],[f24633]) ).
fof(f24637,definition,
( spl56_1305
<=> vd684 = vangle(sK4,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl56_1305])],[avatar_definition]) ).
fof(f24638,plain,
( vd684 = vangle(sK4,sK6,sK5)
| ~ spl56_1305 ),
inference(avatar_component_clause,[],[f24637]) ).
fof(f24639,plain,
( vd684 != vangle(sK4,sK6,sK5)
| spl56_1305 ),
inference(avatar_component_clause,[],[f24637]) ).
fof(f24642,definition,
( spl56_1306
<=> ! [X0] :
( ron(sK4,X0)
| ~ rline(X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl56_1306])],[avatar_definition]) ).
fof(f24643,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ron(sK4,X0)
| ~ ron(sK5,X0) )
| ~ spl56_1306 ),
inference(avatar_component_clause,[],[f24642]) ).
fof(f24741,definition,
( spl56_1328
<=> rR(sK6,vd1306,sK4) ),
introduced(definition,[new_symbols(definition,[spl56_1328])],[avatar_definition]) ).
fof(f24743,plain,
( ~ rR(sK6,vd1306,sK4)
| spl56_1328 ),
inference(avatar_component_clause,[],[f24741]) ).
fof(f24745,definition,
( spl56_1329
<=> vd684 = vangle(sK4,sK6,vd1306) ),
introduced(definition,[new_symbols(definition,[spl56_1329])],[avatar_definition]) ).
fof(f24747,plain,
( vd684 != vangle(sK4,sK6,vd1306)
| spl56_1329 ),
inference(avatar_component_clause,[],[f24745]) ).
fof(f24748,plain,
( spl56_1289
| ~ spl56_1328
| ~ spl56_1329
| ~ spl56_41 ),
inference(avatar_split_clause,[],[f24481,f2502,f24745,f24741,f24569]) ).
fof(f24770,definition,
( spl56_1334
<=> rR(sK6,sK4,vd1300) ),
introduced(definition,[new_symbols(definition,[spl56_1334])],[avatar_definition]) ).
fof(f24772,plain,
( ~ rR(sK6,sK4,vd1300)
| spl56_1334 ),
inference(avatar_component_clause,[],[f24770]) ).
fof(f24795,definition,
( spl56_1339
<=> rR(sK4,sK5,vd1306) ),
introduced(definition,[new_symbols(definition,[spl56_1339])],[avatar_definition]) ).
fof(f24797,plain,
( ~ rR(sK4,sK5,vd1306)
| spl56_1339 ),
inference(avatar_component_clause,[],[f24795]) ).
fof(f24799,definition,
( spl56_1340
<=> vd684 = vangle(sK4,sK5,vd1300) ),
introduced(definition,[new_symbols(definition,[spl56_1340])],[avatar_definition]) ).
fof(f24801,plain,
( vd684 != vangle(sK4,sK5,vd1300)
| spl56_1340 ),
inference(avatar_component_clause,[],[f24799]) ).
fof(f24805,definition,
( spl56_1341
<=> ! [X0] :
( ~ ron(vd1300,X0)
| ~ rline(X0)
| ~ ron(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl56_1341])],[avatar_definition]) ).
fof(f24806,plain,
( ! [X0] :
( ~ ron(vd1300,X0)
| ~ rline(X0)
| ~ ron(sK5,X0) )
| ~ spl56_1341 ),
inference(avatar_component_clause,[],[f24805]) ).
fof(f24808,definition,
( spl56_1342
<=> rR(sK5,vd1300,sK4) ),
introduced(definition,[new_symbols(definition,[spl56_1342])],[avatar_definition]) ).
fof(f24809,plain,
( rR(sK5,vd1300,sK4)
| ~ spl56_1342 ),
inference(avatar_component_clause,[],[f24808]) ).
fof(f24810,plain,
( ~ rR(sK5,vd1300,sK4)
| spl56_1342 ),
inference(avatar_component_clause,[],[f24808]) ).
fof(f24811,plain,
( spl56_1341
| ~ spl56_1342
| ~ spl56_1340
| spl56_13
| spl56_15 ),
inference(avatar_split_clause,[],[f24501,f1807,f1788,f24799,f24808,f24805]) ).
fof(f24943,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,[],[f1899,f987]) ).
fof(f24956,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,[],[f24943]) ).
fof(f25078,definition,
( spl56_1362
<=> ron(sK5,vd1297) ),
introduced(definition,[new_symbols(definition,[spl56_1362])],[avatar_definition]) ).
fof(f25079,plain,
( ron(sK5,vd1297)
| ~ spl56_1362 ),
inference(avatar_component_clause,[],[f25078]) ).
fof(f25212,plain,
( vd684 = vangle(sK4,sK6,sK5)
| ~ ron(sK4,vd1295)
| ~ ron(sK6,vd1295)
| sK5 = sK6
| sK4 = sK6
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| rR(sK4,vd1303,sK5)
| ~ rpoint(sK5) ),
inference(resolution,[],[f23551,f1779]) ).
fof(f25301,definition,
( spl56_1369
<=> ron(sK4,vd1295) ),
introduced(definition,[new_symbols(definition,[spl56_1369])],[avatar_definition]) ).
fof(f25302,plain,
( ron(sK4,vd1295)
| ~ spl56_1369 ),
inference(avatar_component_clause,[],[f25301]) ).
fof(f25303,plain,
( ~ ron(sK4,vd1295)
| spl56_1369 ),
inference(avatar_component_clause,[],[f25301]) ).
fof(f25308,definition,
( spl56_1370
<=> rR(sK4,vd1303,sK5) ),
introduced(definition,[new_symbols(definition,[spl56_1370])],[avatar_definition]) ).
fof(f25309,plain,
( ~ rR(sK4,vd1303,sK5)
| spl56_1370 ),
inference(avatar_component_clause,[],[f25308]) ).
fof(f25396,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,[],[f23536,f788]) ).
fof(f25411,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,[],[f25396,f784]) ).
fof(f25419,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,[],[f25411,f475]) ).
fof(f25498,plain,
! [X2,X3,X0,X1] :
( rR(sK6,X0,vd1300)
| sK6 = X1
| vd1300 = sK6
| sK6 = X2
| sK6 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK6,X2,X1)
| ~ ron(X0,vd1295)
| vangle(vd1300,sK6,X1) = vangle(X0,sK6,X2)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(vd1300)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f23538,f789]) ).
fof(f25512,plain,
! [X2,X3,X0,X1] :
( rR(sK6,X0,vd1300)
| sK6 = X1
| sK6 = X2
| sK6 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK6,X2,X1)
| ~ ron(X0,vd1295)
| vangle(vd1300,sK6,X1) = vangle(X0,sK6,X2)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(vd1300)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f25498,f791]) ).
fof(f25514,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,X3)
| sK6 = X1
| sK6 = X2
| sK6 = X0
| ~ ron(X1,X3)
| rR(sK6,X0,vd1300)
| rR(sK6,X2,X1)
| ~ ron(X0,vd1295)
| vangle(vd1300,sK6,X1) = vangle(X0,sK6,X2)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f25512,f545]) ).
fof(f25532,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,[],[f25419,f790]) ).
fof(f25546,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,[],[f25532,f784]) ).
fof(f25561,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,[],[f25546,f516]) ).
fof(f25576,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,[],[f25561,f475]) ).
fof(f25591,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,[],[f23535,f786]) ).
fof(f25603,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,[],[f25591,f784]) ).
fof(f25607,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,[],[f25603,f479]) ).
fof(f25684,plain,
! [X0,X1] :
( sK6 = X0
| sK4 = sK6
| sK6 = X1
| ~ ron(X0,vd1297)
| rR(sK6,X1,sK4)
| rR(sK6,sK4,X0)
| ~ ron(X1,vd1297)
| vangle(sK4,sK6,X0) = vangle(X1,sK6,sK4)
| ~ rline(vd1297)
| ~ rpoint(X0)
| ~ rpoint(sK4)
| ~ rpoint(X1) ),
inference(resolution,[],[f25607,f786]) ).
fof(f25687,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,[],[f25607,f787]) ).
fof(f25702,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,[],[f25687,f785]) ).
fof(f25704,plain,
! [X0,X1] :
( sK6 = X0
| sK6 = X1
| ~ ron(X0,vd1297)
| rR(sK6,X1,sK4)
| rR(sK6,sK4,X0)
| ~ ron(X1,vd1297)
| vangle(sK4,sK6,X0) = vangle(X1,sK6,sK4)
| ~ rline(vd1297)
| ~ rpoint(X0)
| ~ rpoint(sK4)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25684,f784]) ).
fof(f25716,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,[],[f25702,f516]) ).
fof(f25718,plain,
! [X0,X1] :
( sK6 = X0
| sK6 = X1
| ~ ron(X0,vd1297)
| rR(sK6,X1,sK4)
| rR(sK6,sK4,X0)
| ~ ron(X1,vd1297)
| vangle(sK4,sK6,X0) = vangle(X1,sK6,sK4)
| ~ rpoint(X0)
| ~ rpoint(sK4)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25704,f513]) ).
fof(f25730,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,[],[f25716,f477]) ).
fof(f25732,plain,
! [X0,X1] :
( rR(sK6,sK4,X0)
| rR(sK6,X1,sK4)
| ~ ron(X0,vd1297)
| sK6 = X1
| sK6 = X0
| ~ ron(X1,vd1297)
| vangle(sK4,sK6,X0) = vangle(X1,sK6,sK4)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25718,f479]) ).
fof(f25922,plain,
! [X0,X1] :
( sK6 = X0
| sK5 = sK6
| sK6 = X1
| ~ ron(X0,vd1295)
| rR(sK6,X1,vd1300)
| rR(sK6,sK5,X0)
| ~ ron(X1,vd1295)
| vangle(vd1300,sK6,X0) = vangle(X1,sK6,sK5)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(X1) ),
inference(resolution,[],[f25514,f787]) ).
fof(f25937,plain,
! [X0,X1] :
( sK6 = X0
| sK6 = X1
| ~ ron(X0,vd1295)
| rR(sK6,X1,vd1300)
| rR(sK6,sK5,X0)
| ~ ron(X1,vd1295)
| vangle(vd1300,sK6,X0) = vangle(X1,sK6,sK5)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25922,f785]) ).
fof(f25951,plain,
! [X0,X1] :
( sK6 = X0
| sK6 = X1
| ~ ron(X0,vd1295)
| rR(sK6,X1,vd1300)
| rR(sK6,sK5,X0)
| ~ ron(X1,vd1295)
| vangle(vd1300,sK6,X0) = vangle(X1,sK6,sK5)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25937,f516]) ).
fof(f25965,plain,
! [X0,X1] :
( rR(sK6,sK5,X0)
| rR(sK6,X1,vd1300)
| ~ ron(X0,vd1295)
| sK6 = X1
| sK6 = X0
| ~ ron(X1,vd1295)
| vangle(vd1300,sK6,X0) = vangle(X1,sK6,sK5)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f25951,f477]) ).
fof(f25975,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,[],[f24956,f987]) ).
fof(f25988,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,[],[f25975]) ).
fof(f25998,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,[],[f25988,f1581]) ).
fof(f26024,plain,
! [X2,X0,X1] :
( rR(X0,X1,sK5)
| sK5 = X0
| X0 = X2
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,vd1295)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,sK5)
| ~ rline(vd1295)
| ~ rpoint(sK5)
| ~ rpoint(X1) ),
inference(resolution,[],[f25998,f787]) ).
fof(f26040,plain,
! [X2,X0,X1] :
( rR(X0,X1,sK5)
| sK5 = X0
| X0 = X2
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,vd1295)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,sK5)
| ~ rpoint(sK5)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26024,f516]) ).
fof(f26057,plain,
! [X2,X0,X1] :
( ~ ron(X1,vd1295)
| sK5 = X0
| X0 = X2
| X0 = X1
| ~ rpoint(X0)
| rR(X0,X1,sK5)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,sK5)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26040,f477]) ).
fof(f26106,plain,
! [X0] :
( rR(sK6,X0,sK4)
| ~ ron(vd1306,vd1297)
| sK6 = X0
| vd1306 = sK6
| ~ ron(X0,vd1297)
| vangle(X0,sK6,sK4) = vangle(sK4,sK6,vd1306)
| ~ rpoint(vd1306)
| ~ rpoint(X0) ),
inference(resolution,[],[f25732,f771]) ).
fof(f26191,plain,
! [X0] :
( rR(sK6,X0,sK4)
| sK6 = X0
| vd1306 = sK6
| ~ ron(X0,vd1297)
| vangle(X0,sK6,sK4) = vangle(sK4,sK6,vd1306)
| ~ rpoint(vd1306)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26106,f543]) ).
fof(f26219,plain,
! [X0] :
( rR(sK6,X0,sK4)
| sK6 = X0
| ~ ron(X0,vd1297)
| vangle(X0,sK6,sK4) = vangle(sK4,sK6,vd1306)
| ~ rpoint(vd1306)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26191,f793]) ).
fof(f26226,plain,
! [X0] :
( rR(sK6,X0,sK4)
| sK6 = X0
| ~ ron(X0,vd1297)
| vangle(X0,sK6,sK4) = vangle(sK4,sK6,vd1306)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26219,f474]) ).
fof(f26365,plain,
( sK4 = sK6
| ~ ron(sK4,vd1297)
| vangle(sK4,sK6,sK4) = vangle(sK4,sK6,vd1306)
| ~ rpoint(sK4)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(resolution,[],[f26226,f1581]) ).
fof(f26369,plain,
( sK4 = sK6
| ~ ron(sK4,vd1297)
| vangle(sK4,sK6,sK4) = vangle(sK4,sK6,vd1306)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(duplicate_literal_removal,[],[f26365]) ).
fof(f26384,plain,
( ~ ron(sK4,vd1297)
| vangle(sK4,sK6,sK4) = vangle(sK4,sK6,vd1306)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f26369,f784]) ).
fof(f26398,plain,
( vangle(sK4,sK6,sK4) = vangle(sK4,sK6,vd1306)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f26384,f786]) ).
fof(f26412,plain,
( vangle(sK4,sK6,sK4) = vangle(sK4,sK6,vd1306)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f26398,f479]) ).
fof(f26415,plain,
vangle(sK4,sK6,sK4) = vangle(sK4,sK6,vd1306),
inference(forward_subsumption_resolution,[],[f26412,f475]) ).
fof(f26418,plain,
vd684 = vangle(sK4,sK6,vd1306),
inference(forward_demodulation,[],[f26415,f2219]) ).
fof(f26421,plain,
( $false
| spl56_1329 ),
inference(forward_subsumption_resolution,[],[f26418,f24747]) ).
fof(f26422,plain,
spl56_1329,
inference(avatar_contradiction_clause,[],[f26421]) ).
fof(f26658,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,[],[f25730,f1581]) ).
fof(f26685,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,[],[f26658]) ).
fof(f26711,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,[],[f26685,f787]) ).
fof(f26737,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,[],[f26711,f785]) ).
fof(f26752,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,[],[f26737,f477]) ).
fof(f26757,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,[],[f26752,f475]) ).
fof(f27777,plain,
! [X0] :
( rR(sK4,sK6,X0)
| ~ ron(X0,vd1295)
| sK4 = sK6
| sK4 = X0
| ~ ron(sK6,vd1297)
| vangle(sK6,sK4,sK6) = vangle(sK6,sK4,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK6)
| ~ rpoint(sK4) ),
inference(resolution,[],[f25576,f1581]) ).
fof(f27780,plain,
! [X0] :
( rR(sK4,sK6,X0)
| ~ ron(X0,vd1295)
| sK4 = sK6
| sK4 = X0
| ~ ron(sK6,vd1297)
| vangle(sK6,sK4,sK6) = vangle(sK6,sK4,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK4) ),
inference(duplicate_literal_removal,[],[f27777]) ).
fof(f27808,plain,
! [X0] :
( rR(sK4,sK6,X0)
| ~ ron(X0,vd1295)
| sK4 = X0
| ~ ron(sK6,vd1297)
| vangle(sK6,sK4,sK6) = vangle(sK6,sK4,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f27780,f784]) ).
fof(f27834,plain,
! [X0] :
( rR(sK4,sK6,X0)
| ~ ron(X0,vd1295)
| sK4 = X0
| vangle(sK6,sK4,sK6) = vangle(sK6,sK4,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f27808,f788]) ).
fof(f27860,plain,
! [X0] :
( rR(sK4,sK6,X0)
| ~ ron(X0,vd1295)
| sK4 = X0
| vangle(sK6,sK4,sK6) = vangle(sK6,sK4,X0)
| ~ rpoint(X0)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f27834,f475]) ).
fof(f27865,plain,
! [X0] :
( rR(sK4,sK6,X0)
| ~ ron(X0,vd1295)
| sK4 = X0
| vangle(sK6,sK4,sK6) = vangle(sK6,sK4,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f27860,f479]) ).
fof(f27869,plain,
! [X0] :
( rR(sK4,sK6,X0)
| vd684 = vangle(sK6,sK4,X0)
| ~ ron(X0,vd1295)
| sK4 = X0
| ~ rpoint(X0) ),
inference(forward_demodulation,[],[f27865,f2012]) ).
fof(f27945,plain,
( ~ rR(sK6,sK4,vd1300)
| ~ rpoint(vd1300)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ spl56_1284 ),
inference(resolution,[],[f24539,f965]) ).
fof(f27962,plain,
( ~ rR(sK6,sK4,vd1300)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ spl56_1284 ),
inference(forward_subsumption_resolution,[],[f27945,f545]) ).
fof(f27974,plain,
( ~ rR(sK6,sK4,vd1300)
| ~ rpoint(sK4)
| ~ spl56_1284 ),
inference(forward_subsumption_resolution,[],[f27962,f475]) ).
fof(f27985,plain,
( ~ rR(sK6,sK4,vd1300)
| ~ spl56_1284 ),
inference(forward_subsumption_resolution,[],[f27974,f479]) ).
fof(f27991,plain,
( ~ spl56_1334
| ~ spl56_1284 ),
inference(avatar_split_clause,[],[f27985,f24538,f24770]) ).
fof(f28022,plain,
( ~ rline(vd1297)
| ~ ron(sK4,vd1297)
| ron(sK5,vd1297)
| ~ spl56_1286 ),
inference(resolution,[],[f24553,f788]) ).
fof(f28030,plain,
( ~ ron(sK4,vd1297)
| ron(sK5,vd1297)
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f28022,f513]) ).
fof(f28033,plain,
( ron(sK5,vd1297)
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f28030,f786]) ).
fof(f28037,plain,
( ~ rR(sK4,vd1303,sK5)
| ~ rpoint(sK5)
| ~ spl56_1282 ),
inference(resolution,[],[f24530,f1983]) ).
fof(f28040,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| ~ spl56_1282 ),
inference(resolution,[],[f24530,f962]) ).
fof(f28044,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| ~ spl56_1282 ),
inference(resolution,[],[f24530,f1047]) ).
fof(f28055,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| ~ spl56_1282 ),
inference(forward_subsumption_resolution,[],[f28044,f477]) ).
fof(f28059,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| ~ spl56_1282 ),
inference(forward_subsumption_resolution,[],[f28040,f477]) ).
fof(f28061,plain,
( ~ rR(sK4,vd1303,sK5)
| ~ spl56_1282 ),
inference(forward_subsumption_resolution,[],[f28037,f477]) ).
fof(f28067,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK6) )
| ~ spl56_1282 ),
inference(forward_subsumption_resolution,[],[f28055,f479]) ).
fof(f28071,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK6) )
| ~ spl56_1282 ),
inference(forward_subsumption_resolution,[],[f28059,f479]) ).
fof(f28073,plain,
( ~ spl56_1370
| ~ spl56_1282 ),
inference(avatar_split_clause,[],[f28061,f24529,f25308]) ).
fof(f28079,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ron(sK4,X0)
| ~ rline(X0) )
| ~ spl56_1282 ),
inference(forward_subsumption_resolution,[],[f28067,f475]) ).
fof(f28083,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ron(sK5,X0)
| ~ rline(X0) )
| ~ spl56_1282 ),
inference(forward_subsumption_resolution,[],[f28071,f475]) ).
fof(f28086,plain,
( spl56_1306
| ~ spl56_1282 ),
inference(avatar_split_clause,[],[f28079,f24529,f24642]) ).
fof(f28089,plain,
( spl56_1286
| ~ spl56_1282 ),
inference(avatar_split_clause,[],[f28083,f24529,f24552]) ).
fof(f28094,plain,
( spl56_1362
| ~ spl56_1286 ),
inference(avatar_split_clause,[],[f28033,f24552,f25078]) ).
fof(f28181,plain,
( ! [X0] :
( ~ rline(sK7(sK6,X0))
| ~ ron(sK4,sK7(sK6,X0))
| ron(sK5,sK7(sK6,X0))
| sK6 = X0
| ~ rpoint(X0)
| ~ rpoint(sK6) )
| ~ spl56_1286 ),
inference(resolution,[],[f24553,f989]) ).
fof(f28184,plain,
( ! [X0] :
( ~ ron(sK4,sK7(sK6,X0))
| ron(sK5,sK7(sK6,X0))
| sK6 = X0
| ~ rpoint(X0)
| ~ rpoint(sK6) )
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f28181,f991]) ).
fof(f28186,plain,
( ! [X0] :
( ~ ron(sK4,sK7(sK6,X0))
| ron(sK5,sK7(sK6,X0))
| sK6 = X0
| ~ rpoint(X0) )
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f28184,f475]) ).
fof(f28650,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1300,X0)
| ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(vd1300) )
| ~ spl56_1342 ),
inference(resolution,[],[f24809,f1047]) ).
fof(f28661,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1300,X0)
| ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1300) )
| ~ spl56_1342 ),
inference(forward_subsumption_resolution,[],[f28650,f479]) ).
fof(f28672,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1300,X0)
| ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(vd1300) )
| ~ spl56_1342 ),
inference(forward_subsumption_resolution,[],[f28661,f477]) ).
fof(f28683,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1300,X0)
| ron(sK5,X0)
| ~ rline(X0) )
| ~ spl56_1342 ),
inference(forward_subsumption_resolution,[],[f28672,f545]) ).
fof(f28690,plain,
( spl56_1302
| ~ spl56_1342 ),
inference(avatar_split_clause,[],[f28683,f24808,f24626]) ).
fof(f28738,plain,
( ! [X0] :
( vd684 != vd684
| ~ rR(sK6,sK4,sK5)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| sK5 = sK6
| sK4 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| ~ spl56_1305 ),
inference(superposition,[],[f902,f24638]) ).
fof(f28739,plain,
( ! [X0] :
( ~ rR(sK6,sK4,sK5)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| sK5 = sK6
| sK4 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| ~ spl56_1305 ),
inference(trivial_inequality_removal,[],[f28738]) ).
fof(f28741,plain,
( ! [X0] :
( ~ rR(sK6,sK4,sK5)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| sK4 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| ~ spl56_1305 ),
inference(forward_subsumption_resolution,[],[f28739,f785]) ).
fof(f28742,plain,
( ! [X0] :
( ~ rR(sK6,sK4,sK5)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| ~ spl56_1305 ),
inference(forward_subsumption_resolution,[],[f28741,f784]) ).
fof(f28743,plain,
( ! [X0] :
( ~ rR(sK6,sK4,sK5)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| ~ spl56_1305 ),
inference(forward_subsumption_resolution,[],[f28742,f477]) ).
fof(f28744,plain,
( ! [X0] :
( ~ rR(sK6,sK4,sK5)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK6) )
| ~ spl56_1305 ),
inference(forward_subsumption_resolution,[],[f28743,f479]) ).
fof(f28745,plain,
( ! [X0] :
( ~ rR(sK6,sK4,sK5)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0) )
| ~ spl56_1305 ),
inference(forward_subsumption_resolution,[],[f28744,f475]) ).
fof(f28747,definition,
( spl56_1394
<=> rR(sK6,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl56_1394])],[avatar_definition]) ).
fof(f28748,plain,
( rR(sK6,sK4,sK5)
| ~ spl56_1394 ),
inference(avatar_component_clause,[],[f28747]) ).
fof(f28749,plain,
( ~ rR(sK6,sK4,sK5)
| spl56_1394 ),
inference(avatar_component_clause,[],[f28747]) ).
fof(f28750,plain,
( spl56_1281
| ~ spl56_1394
| ~ spl56_1305 ),
inference(avatar_split_clause,[],[f28745,f24637,f28747,f24526]) ).
fof(f28880,plain,
( vd684 = vangle(sK6,sK4,vd1300)
| ~ ron(vd1300,vd1295)
| vd1300 = sK4
| ~ rpoint(vd1300)
| spl56_1284 ),
inference(resolution,[],[f24540,f27869]) ).
fof(f28885,plain,
( vd684 = vangle(sK6,sK4,vd1300)
| vd1300 = sK4
| ~ rpoint(vd1300)
| spl56_1284 ),
inference(forward_subsumption_resolution,[],[f28880,f789]) ).
fof(f28887,plain,
( vd684 = vangle(sK6,sK4,vd1300)
| ~ rpoint(vd1300)
| spl56_13
| spl56_1284 ),
inference(forward_subsumption_resolution,[],[f28885,f1789]) ).
fof(f28889,plain,
( vd684 = vangle(sK6,sK4,vd1300)
| spl56_13
| spl56_1284 ),
inference(forward_subsumption_resolution,[],[f28887,f545]) ).
fof(f28891,plain,
( vd684 = sF55
| spl56_13
| spl56_1284 ),
inference(forward_demodulation,[],[f28889,f1577]) ).
fof(f30773,plain,
( rR(sK6,sK5,sK4)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ spl56_1394 ),
inference(resolution,[],[f28748,f976]) ).
fof(f30787,plain,
( ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| spl56_1304
| ~ spl56_1394 ),
inference(forward_subsumption_resolution,[],[f30773,f24635]) ).
fof(f30795,plain,
( ~ rpoint(sK6)
| ~ rpoint(sK4)
| spl56_1304
| ~ spl56_1394 ),
inference(forward_subsumption_resolution,[],[f30787,f477]) ).
fof(f30803,plain,
( ~ rpoint(sK4)
| spl56_1304
| ~ spl56_1394 ),
inference(forward_subsumption_resolution,[],[f30795,f475]) ).
fof(f30806,plain,
( $false
| spl56_1304
| ~ spl56_1394 ),
inference(forward_subsumption_resolution,[],[f30803,f479]) ).
fof(f30807,plain,
( spl56_1304
| ~ spl56_1394 ),
inference(avatar_contradiction_clause,[],[f30806]) ).
fof(f30898,plain,
( rR(sK5,vd1300,sK4)
| ~ rpoint(sK4)
| ~ spl56_1304 ),
inference(resolution,[],[f24634,f1780]) ).
fof(f30915,plain,
( ~ rpoint(sK4)
| ~ spl56_1304
| spl56_1342 ),
inference(forward_subsumption_resolution,[],[f30898,f24810]) ).
fof(f30921,plain,
( $false
| ~ spl56_1304
| spl56_1342 ),
inference(forward_subsumption_resolution,[],[f30915,f479]) ).
fof(f30922,plain,
( ~ spl56_1304
| spl56_1342 ),
inference(avatar_contradiction_clause,[],[f30921]) ).
fof(f31379,plain,
( ~ rline(vd1297)
| ~ ron(sK4,vd1297)
| ~ spl56_1281 ),
inference(resolution,[],[f24527,f788]) ).
fof(f31388,plain,
( ~ ron(sK4,vd1297)
| ~ spl56_1281 ),
inference(forward_subsumption_resolution,[],[f31379,f513]) ).
fof(f31393,plain,
( $false
| ~ spl56_1281 ),
inference(forward_subsumption_resolution,[],[f31388,f786]) ).
fof(f31394,plain,
~ spl56_1281,
inference(avatar_contradiction_clause,[],[f31393]) ).
fof(f31395,plain,
( ~ rline(vd1297)
| ~ ron(sK4,vd1297)
| ~ spl56_1278
| ~ spl56_1362 ),
inference(resolution,[],[f24515,f25079]) ).
fof(f31405,plain,
( ~ ron(sK4,vd1297)
| ~ spl56_1278
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f31395,f513]) ).
fof(f31410,plain,
( $false
| ~ spl56_1278
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f31405,f786]) ).
fof(f31411,plain,
( ~ spl56_1278
| ~ spl56_1362 ),
inference(avatar_contradiction_clause,[],[f31410]) ).
fof(f31523,plain,
( ~ rline(vd1295)
| ~ ron(sK5,vd1295)
| ~ spl56_1303 ),
inference(resolution,[],[f24631,f790]) ).
fof(f31530,plain,
( ~ ron(sK5,vd1295)
| ~ spl56_1303 ),
inference(forward_subsumption_resolution,[],[f31523,f516]) ).
fof(f31534,plain,
( $false
| ~ spl56_1303 ),
inference(forward_subsumption_resolution,[],[f31530,f787]) ).
fof(f31535,plain,
~ spl56_1303,
inference(avatar_contradiction_clause,[],[f31534]) ).
fof(f31678,plain,
( ~ rline(vd1295)
| ~ ron(vd1300,vd1295)
| ~ spl56_1300
| ~ spl56_1369 ),
inference(resolution,[],[f24619,f25302]) ).
fof(f31686,plain,
( ~ ron(vd1300,vd1295)
| ~ spl56_1300
| ~ spl56_1369 ),
inference(forward_subsumption_resolution,[],[f31678,f516]) ).
fof(f31689,plain,
( $false
| ~ spl56_1300
| ~ spl56_1369 ),
inference(forward_subsumption_resolution,[],[f31686,f789]) ).
fof(f31690,plain,
( ~ spl56_1300
| ~ spl56_1369 ),
inference(avatar_contradiction_clause,[],[f31689]) ).
fof(f31691,plain,
( ! [X0] :
( ~ rline(X0)
| ~ ron(sK4,X0)
| ~ ron(vd1300,X0) )
| ~ spl56_1302
| ~ spl56_1341 ),
inference(forward_subsumption_resolution,[],[f24627,f24806]) ).
fof(f31692,plain,
( spl56_1300
| ~ spl56_1302
| ~ spl56_1341 ),
inference(avatar_split_clause,[],[f31691,f24805,f24626,f24618]) ).
fof(f32914,plain,
( spl56_1285
| spl56_13
| spl56_1284 ),
inference(avatar_split_clause,[],[f28891,f24538,f1788,f24542]) ).
fof(f33041,plain,
( ~ rline(vd1297)
| ~ ron(vd1306,vd1297)
| ~ spl56_1289 ),
inference(resolution,[],[f24570,f788]) ).
fof(f33050,plain,
( ~ ron(vd1306,vd1297)
| ~ spl56_1289 ),
inference(forward_subsumption_resolution,[],[f33041,f513]) ).
fof(f33055,plain,
( $false
| ~ spl56_1289 ),
inference(forward_subsumption_resolution,[],[f33050,f543]) ).
fof(f33056,plain,
~ spl56_1289,
inference(avatar_contradiction_clause,[],[f33055]) ).
fof(f33834,definition,
( spl56_1403
<=> vd1297 = vd1295 ),
introduced(definition,[new_symbols(definition,[spl56_1403])],[avatar_definition]) ).
fof(f33835,plain,
( vd1297 != vd1295
| spl56_1403 ),
inference(avatar_component_clause,[],[f33834]) ).
fof(f33836,plain,
( vd1297 = vd1295
| ~ spl56_1403 ),
inference(avatar_component_clause,[],[f33834]) ).
fof(f33957,plain,
! [X0] :
( rR(sK6,X0,vd1300)
| ~ ron(vd1300,vd1295)
| sK6 = X0
| vd1300 = sK6
| ~ ron(X0,vd1295)
| vangle(vd1300,sK6,vd1300) = vangle(X0,sK6,sK5)
| ~ rpoint(vd1300)
| ~ rpoint(X0) ),
inference(resolution,[],[f25965,f774]) ).
fof(f34041,plain,
! [X0] :
( rR(sK6,X0,vd1300)
| sK6 = X0
| vd1300 = sK6
| ~ ron(X0,vd1295)
| vangle(vd1300,sK6,vd1300) = vangle(X0,sK6,sK5)
| ~ rpoint(vd1300)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f33957,f789]) ).
fof(f34073,plain,
! [X0] :
( rR(sK6,X0,vd1300)
| sK6 = X0
| ~ ron(X0,vd1295)
| vangle(vd1300,sK6,vd1300) = vangle(X0,sK6,sK5)
| ~ rpoint(vd1300)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f34041,f791]) ).
fof(f34105,plain,
! [X0] :
( rR(sK6,X0,vd1300)
| sK6 = X0
| ~ ron(X0,vd1295)
| vangle(vd1300,sK6,vd1300) = vangle(X0,sK6,sK5)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f34073,f545]) ).
fof(f35208,plain,
! [X0,X1] :
( sK5 = X0
| X0 = X1
| sK6 = X0
| ~ rpoint(X0)
| rR(X0,sK6,sK5)
| ~ rpoint(X1)
| vangle(X1,X0,sK5) = vangle(X1,X0,sK6)
| ~ rpoint(sK6) ),
inference(resolution,[],[f26057,f790]) ).
fof(f35221,plain,
! [X0,X1] :
( ~ rpoint(X1)
| X0 = X1
| sK6 = X0
| ~ rpoint(X0)
| rR(X0,sK6,sK5)
| sK5 = X0
| vangle(X1,X0,sK5) = vangle(X1,X0,sK6) ),
inference(forward_subsumption_resolution,[],[f35208,f475]) ).
fof(f35250,plain,
! [X0] :
( sK5 = X0
| sK6 = X0
| ~ rpoint(X0)
| rR(X0,sK6,sK5)
| sK5 = X0
| vangle(sK5,X0,sK5) = vangle(sK5,X0,sK6) ),
inference(resolution,[],[f35221,f477]) ).
fof(f35254,plain,
! [X0] :
( rR(X0,sK6,sK5)
| sK6 = X0
| ~ rpoint(X0)
| sK5 = X0
| vangle(sK5,X0,sK5) = vangle(sK5,X0,sK6) ),
inference(duplicate_literal_removal,[],[f35250]) ).
fof(f35299,plain,
( ron(sK5,sK7(sK6,sK4))
| sK4 = sK6
| ~ rpoint(sK4)
| sK4 = sK6
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ spl56_1286 ),
inference(resolution,[],[f28186,f987]) ).
fof(f35300,plain,
( ron(sK5,sK7(sK6,sK4))
| sK4 = sK6
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ spl56_1286 ),
inference(duplicate_literal_removal,[],[f35299]) ).
fof(f35301,plain,
( ron(sK5,sK7(sK6,sK4))
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35300,f784]) ).
fof(f35302,plain,
( ron(sK5,sK7(sK6,sK4))
| ~ rpoint(sK6)
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35301,f479]) ).
fof(f35303,plain,
( ron(sK5,sK7(sK6,sK4))
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35302,f475]) ).
fof(f35452,definition,
( spl56_1422
<=> vd1297 = sK7(sK6,sK4) ),
introduced(definition,[new_symbols(definition,[spl56_1422])],[avatar_definition]) ).
fof(f35454,plain,
( vd1297 = sK7(sK6,sK4)
| ~ spl56_1422 ),
inference(avatar_component_clause,[],[f35452]) ).
fof(f35527,plain,
( ! [X0] :
( ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ ron(sK5,X0)
| sK4 = sK6
| ~ ron(sK4,X0)
| sK7(sK6,sK4) = X0
| ~ rline(X0)
| sK4 = sK5
| ~ rpoint(sK5) )
| ~ spl56_1286 ),
inference(resolution,[],[f1883,f35303]) ).
fof(f35547,plain,
( ! [X0] :
( ~ rpoint(sK6)
| ~ ron(sK5,X0)
| sK4 = sK6
| ~ ron(sK4,X0)
| sK7(sK6,sK4) = X0
| ~ rline(X0)
| sK4 = sK5
| ~ rpoint(sK5) )
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35527,f479]) ).
fof(f35551,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| sK4 = sK6
| ~ ron(sK4,X0)
| sK7(sK6,sK4) = X0
| ~ rline(X0)
| sK4 = sK5
| ~ rpoint(sK5) )
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35547,f475]) ).
fof(f35555,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| sK7(sK6,sK4) = X0
| ~ rline(X0)
| sK4 = sK5
| ~ rpoint(sK5) )
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35551,f784]) ).
fof(f35556,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| sK7(sK6,sK4) = X0
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35555,f760]) ).
fof(f35557,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| sK7(sK6,sK4) = X0
| ~ rline(X0) )
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35556,f477]) ).
fof(f35558,plain,
( ~ ron(sK4,vd1297)
| vd1297 = sK7(sK6,sK4)
| ~ rline(vd1297)
| ~ spl56_1286
| ~ spl56_1362 ),
inference(resolution,[],[f35557,f25079]) ).
fof(f35569,plain,
( vd1297 = sK7(sK6,sK4)
| ~ rline(vd1297)
| ~ spl56_1286
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f35558,f786]) ).
fof(f35573,plain,
( vd1297 = sK7(sK6,sK4)
| ~ spl56_1286
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f35569,f513]) ).
fof(f35575,plain,
( spl56_1422
| ~ spl56_1286
| ~ spl56_1362 ),
inference(avatar_split_clause,[],[f35573,f25078,f24552,f35452]) ).
fof(f35659,plain,
( ! [X0] :
( ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ ron(sK5,X0)
| sK4 = sK6
| ~ ron(sK6,X0)
| sK7(sK6,sK4) = X0
| ~ rline(X0)
| sK5 = sK6
| ~ rpoint(sK5) )
| ~ spl56_1286 ),
inference(resolution,[],[f1901,f35303]) ).
fof(f35679,plain,
( ! [X0] :
( ~ rpoint(sK6)
| ~ ron(sK5,X0)
| sK4 = sK6
| ~ ron(sK6,X0)
| sK7(sK6,sK4) = X0
| ~ rline(X0)
| sK5 = sK6
| ~ rpoint(sK5) )
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35659,f479]) ).
fof(f35683,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| sK4 = sK6
| ~ ron(sK6,X0)
| sK7(sK6,sK4) = X0
| ~ rline(X0)
| sK5 = sK6
| ~ rpoint(sK5) )
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35679,f475]) ).
fof(f35687,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| sK7(sK6,sK4) = X0
| ~ rline(X0)
| sK5 = sK6
| ~ rpoint(sK5) )
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35683,f784]) ).
fof(f35688,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| sK7(sK6,sK4) = X0
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35687,f785]) ).
fof(f35689,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| sK7(sK6,sK4) = X0
| ~ rline(X0) )
| ~ spl56_1286 ),
inference(forward_subsumption_resolution,[],[f35688,f477]) ).
fof(f35690,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| vd1297 = X0
| ~ rline(X0) )
| ~ spl56_1286
| ~ spl56_1422 ),
inference(forward_demodulation,[],[f35689,f35454]) ).
fof(f35692,plain,
( ~ ron(sK5,vd1295)
| vd1297 = vd1295
| ~ rline(vd1295)
| ~ spl56_1286
| ~ spl56_1422 ),
inference(resolution,[],[f35690,f790]) ).
fof(f36003,plain,
( vd1306 = sK6
| ~ ron(vd1306,vd1297)
| vangle(sK4,sK6,sK5) = vangle(vd1306,sK6,sK5)
| ~ rpoint(vd1306)
| spl56_1328 ),
inference(resolution,[],[f24743,f26757]) ).
fof(f36683,plain,
( sK4 = sK6
| ~ rpoint(sK4)
| sK4 = sK5
| vangle(sK5,sK4,sK5) = vangle(sK5,sK4,sK6)
| spl56_1282 ),
inference(resolution,[],[f35254,f24531]) ).
fof(f36701,plain,
( ~ rpoint(sK4)
| sK4 = sK5
| vangle(sK5,sK4,sK5) = vangle(sK5,sK4,sK6)
| spl56_1282 ),
inference(forward_subsumption_resolution,[],[f36683,f784]) ).
fof(f36716,plain,
( sK4 = sK5
| vangle(sK5,sK4,sK5) = vangle(sK5,sK4,sK6)
| spl56_1282 ),
inference(forward_subsumption_resolution,[],[f36701,f479]) ).
fof(f36731,plain,
( vangle(sK5,sK4,sK5) = vangle(sK5,sK4,sK6)
| spl56_1282 ),
inference(forward_subsumption_resolution,[],[f36716,f760]) ).
fof(f36736,plain,
( sF53 = vangle(sK5,sK4,sK5)
| spl56_1282 ),
inference(forward_demodulation,[],[f36731,f2653]) ).
fof(f36740,plain,
( vd684 = sF53
| spl56_1282 ),
inference(forward_demodulation,[],[f36736,f2013]) ).
fof(f37838,plain,
! [X0] :
( rR(sK6,X0,vd1300)
| vd684 = vangle(X0,sK6,sK5)
| sK6 = X0
| ~ ron(X0,vd1295)
| ~ rpoint(X0) ),
inference(forward_demodulation,[],[f34105,f2220]) ).
fof(f37871,plain,
( vd1297 = vd1295
| ~ rline(vd1295)
| ~ spl56_1286
| ~ spl56_1422 ),
inference(forward_subsumption_resolution,[],[f35692,f787]) ).
fof(f37938,plain,
( ~ rline(vd1295)
| ~ spl56_1286
| spl56_1403
| ~ spl56_1422 ),
inference(forward_subsumption_resolution,[],[f37871,f33835]) ).
fof(f37959,plain,
( $false
| ~ spl56_1286
| spl56_1403
| ~ spl56_1422 ),
inference(forward_subsumption_resolution,[],[f37938,f516]) ).
fof(f37960,plain,
( ~ spl56_1286
| spl56_1403
| ~ spl56_1422 ),
inference(avatar_contradiction_clause,[],[f37959]) ).
fof(f37982,plain,
( vd684 = vangle(sK4,sK6,sK5)
| sK4 = sK6
| ~ ron(sK4,vd1295)
| ~ rpoint(sK4)
| spl56_1334 ),
inference(resolution,[],[f37838,f24772]) ).
fof(f38542,plain,
( ~ rR(sK4,sK5,vd1306)
| ~ rpoint(vd1306)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ spl56_1279 ),
inference(resolution,[],[f24518,f965]) ).
fof(f38557,plain,
( ~ rR(sK4,sK5,vd1306)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ spl56_1279 ),
inference(forward_subsumption_resolution,[],[f38542,f474]) ).
fof(f38566,plain,
( ~ rR(sK4,sK5,vd1306)
| ~ rpoint(sK5)
| ~ spl56_1279 ),
inference(forward_subsumption_resolution,[],[f38557,f479]) ).
fof(f38575,plain,
( ~ rR(sK4,sK5,vd1306)
| ~ spl56_1279 ),
inference(forward_subsumption_resolution,[],[f38566,f477]) ).
fof(f38579,plain,
( ~ spl56_1339
| ~ spl56_1279 ),
inference(avatar_split_clause,[],[f38575,f24517,f24795]) ).
fof(f38642,plain,
( vd684 = vangle(sK5,sK4,vd1306)
| ~ ron(sK5,vd1297)
| ~ ron(sK4,vd1297)
| vd1306 = sK4
| sK4 = sK5
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| spl56_1339 ),
inference(resolution,[],[f24797,f23548]) ).
fof(f38643,plain,
( vd684 = vangle(sK5,sK4,vd1306)
| ~ ron(sK4,vd1297)
| vd1306 = sK4
| sK4 = sK5
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| spl56_1339
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f38642,f25079]) ).
fof(f38646,plain,
( vd684 = vangle(sK5,sK4,vd1306)
| vd1306 = sK4
| sK4 = sK5
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| spl56_1339
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f38643,f786]) ).
fof(f38649,plain,
( vd684 = vangle(sK5,sK4,vd1306)
| sK4 = sK5
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| spl56_30
| spl56_1339
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f38646,f2034]) ).
fof(f38652,plain,
( vd684 = vangle(sK5,sK4,vd1306)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| spl56_30
| spl56_1339
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f38649,f760]) ).
fof(f38655,plain,
( vd684 = vangle(sK5,sK4,vd1306)
| ~ rpoint(sK4)
| spl56_30
| spl56_1339
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f38652,f477]) ).
fof(f38656,plain,
( vd684 = vangle(sK5,sK4,vd1306)
| spl56_30
| spl56_1339
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f38655,f479]) ).
fof(f38657,plain,
( vd684 = vangle(sK4,sK5,vd1300)
| spl56_13
| spl56_30
| spl56_39
| spl56_1339
| ~ spl56_1362 ),
inference(forward_demodulation,[],[f38656,f15713]) ).
fof(f38658,plain,
( $false
| spl56_13
| spl56_30
| spl56_39
| spl56_1339
| spl56_1340
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f38657,f24801]) ).
fof(f38659,plain,
( spl56_13
| spl56_30
| spl56_39
| spl56_1339
| spl56_1340
| ~ spl56_1362 ),
inference(avatar_contradiction_clause,[],[f38658]) ).
fof(f41903,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,[],[f3879,f1103]) ).
fof(f41925,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,[],[f41903]) ).
fof(f41977,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,[],[f41925,f6631]) ).
fof(f42005,plain,
( ! [X0] :
( ~ rpoint(sK6)
| sK4 = sK5
| ~ rpoint(sK4)
| sK4 = sK6
| rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1295 ),
inference(forward_subsumption_resolution,[],[f41977,f24597]) ).
fof(f42013,plain,
( ! [X0] :
( sK4 = sK5
| ~ rpoint(sK4)
| sK4 = sK6
| rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1295 ),
inference(forward_subsumption_resolution,[],[f42005,f475]) ).
fof(f42021,plain,
( ! [X0] :
( ~ rpoint(sK4)
| sK4 = sK6
| rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1295 ),
inference(forward_subsumption_resolution,[],[f42013,f760]) ).
fof(f42029,plain,
( ! [X0] :
( sK4 = sK6
| rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1295 ),
inference(forward_subsumption_resolution,[],[f42021,f479]) ).
fof(f42033,plain,
( ! [X0] :
( rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1295 ),
inference(forward_subsumption_resolution,[],[f42029,f784]) ).
fof(f42037,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1295
| spl56_1394 ),
inference(forward_subsumption_resolution,[],[f42033,f28749]) ).
fof(f42048,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0) )
| ~ spl56_1295
| spl56_1394 ),
inference(forward_subsumption_resolution,[],[f42037,f477]) ).
fof(f42051,plain,
( spl56_1278
| ~ spl56_1295
| spl56_1394 ),
inference(avatar_split_clause,[],[f42048,f28747,f24596,f24514]) ).
fof(f42122,plain,
( ! [X0] :
( ~ rpoint(sK6)
| sK4 = sK5
| ~ rpoint(sK4)
| sK4 = sK6
| rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1306 ),
inference(forward_subsumption_resolution,[],[f41977,f24643]) ).
fof(f42676,plain,
( ! [X0] :
( sK4 = sK5
| ~ rpoint(sK4)
| sK4 = sK6
| rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1306 ),
inference(forward_subsumption_resolution,[],[f42122,f475]) ).
fof(f42945,plain,
( ! [X0] :
( ~ rpoint(sK4)
| sK4 = sK6
| rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1306 ),
inference(forward_subsumption_resolution,[],[f42676,f760]) ).
fof(f43139,plain,
( ! [X0] :
( sK4 = sK6
| rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1306 ),
inference(forward_subsumption_resolution,[],[f42945,f479]) ).
fof(f43262,plain,
( ! [X0] :
( rR(sK6,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1306 ),
inference(forward_subsumption_resolution,[],[f43139,f784]) ).
fof(f43327,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl56_1306
| spl56_1394 ),
inference(forward_subsumption_resolution,[],[f43262,f28749]) ).
fof(f43355,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0) )
| ~ spl56_1306
| spl56_1394 ),
inference(forward_subsumption_resolution,[],[f43327,f477]) ).
fof(f43365,plain,
( spl56_1303
| ~ spl56_1306
| spl56_1394 ),
inference(avatar_split_clause,[],[f43355,f28747,f24642,f24630]) ).
fof(f43395,plain,
( spl56_1283
| spl56_1282 ),
inference(avatar_split_clause,[],[f36740,f24529,f24533]) ).
fof(f43408,plain,
( ~ ron(sK4,vd1297)
| spl56_1369
| ~ spl56_1403 ),
inference(forward_demodulation,[],[f25303,f33836]) ).
fof(f43577,plain,
( ~ ron(sK4,vd1295)
| ~ ron(sK6,vd1295)
| sK5 = sK6
| sK4 = sK6
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| rR(sK4,vd1303,sK5)
| ~ rpoint(sK5)
| spl56_1305 ),
inference(forward_subsumption_resolution,[],[f25212,f24639]) ).
fof(f43617,plain,
( sK4 = sK6
| ~ ron(sK4,vd1295)
| ~ rpoint(sK4)
| spl56_1305
| spl56_1334 ),
inference(forward_subsumption_resolution,[],[f37982,f24639]) ).
fof(f44085,plain,
( $false
| spl56_1369
| ~ spl56_1403 ),
inference(forward_subsumption_resolution,[],[f43408,f786]) ).
fof(f44086,plain,
( spl56_1369
| ~ spl56_1403 ),
inference(avatar_contradiction_clause,[],[f44085]) ).
fof(f44197,plain,
( ~ ron(sK4,vd1295)
| sK5 = sK6
| sK4 = sK6
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| rR(sK4,vd1303,sK5)
| ~ rpoint(sK5)
| spl56_1305 ),
inference(forward_subsumption_resolution,[],[f43577,f790]) ).
fof(f44208,plain,
( ~ ron(sK4,vd1295)
| ~ rpoint(sK4)
| spl56_1305
| spl56_1334 ),
inference(forward_subsumption_resolution,[],[f43617,f784]) ).
fof(f44634,plain,
( ~ ron(sK4,vd1295)
| sK4 = sK6
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| rR(sK4,vd1303,sK5)
| ~ rpoint(sK5)
| spl56_1305 ),
inference(forward_subsumption_resolution,[],[f44197,f785]) ).
fof(f44640,plain,
( ~ ron(sK4,vd1295)
| spl56_1305
| spl56_1334 ),
inference(forward_subsumption_resolution,[],[f44208,f479]) ).
fof(f44951,plain,
( ~ ron(sK4,vd1295)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| rR(sK4,vd1303,sK5)
| ~ rpoint(sK5)
| spl56_1305 ),
inference(forward_subsumption_resolution,[],[f44634,f784]) ).
fof(f44955,plain,
( ~ ron(sK4,vd1297)
| spl56_1305
| spl56_1334
| ~ spl56_1403 ),
inference(forward_demodulation,[],[f44640,f33836]) ).
fof(f45141,plain,
( ~ ron(sK4,vd1295)
| ~ rpoint(sK6)
| rR(sK4,vd1303,sK5)
| ~ rpoint(sK5)
| spl56_1305 ),
inference(forward_subsumption_resolution,[],[f44951,f479]) ).
fof(f45143,plain,
( $false
| spl56_1305
| spl56_1334
| ~ spl56_1403 ),
inference(forward_subsumption_resolution,[],[f44955,f786]) ).
fof(f45144,plain,
( spl56_1305
| spl56_1334
| ~ spl56_1403 ),
inference(avatar_contradiction_clause,[],[f45143]) ).
fof(f45275,plain,
( ~ ron(sK4,vd1295)
| rR(sK4,vd1303,sK5)
| ~ rpoint(sK5)
| spl56_1305 ),
inference(forward_subsumption_resolution,[],[f45141,f475]) ).
fof(f45382,plain,
( ~ ron(sK4,vd1295)
| ~ rpoint(sK5)
| spl56_1305
| spl56_1370 ),
inference(forward_subsumption_resolution,[],[f45275,f25309]) ).
fof(f45454,plain,
( ~ ron(sK4,vd1295)
| spl56_1305
| spl56_1370 ),
inference(forward_subsumption_resolution,[],[f45382,f477]) ).
fof(f45491,plain,
( ~ ron(sK4,vd1297)
| spl56_1305
| spl56_1370
| ~ spl56_1403 ),
inference(forward_demodulation,[],[f45454,f33836]) ).
fof(f45522,plain,
( $false
| spl56_1305
| spl56_1370
| ~ spl56_1403 ),
inference(forward_subsumption_resolution,[],[f45491,f786]) ).
fof(f45523,plain,
( spl56_1305
| spl56_1370
| ~ spl56_1403 ),
inference(avatar_contradiction_clause,[],[f45522]) ).
fof(f46783,plain,
( sF54 = vplus(sF52,vd684)
| ~ spl56_1283 ),
inference(superposition,[],[f1575,f24534]) ).
fof(f46925,plain,
( vd684 != sF54
| ~ spl56_1285 ),
inference(superposition,[],[f1578,f24543]) ).
fof(f47284,plain,
( vd684 = vangle(sK4,sK5,vd1306)
| ~ ron(sK4,vd1297)
| ~ ron(sK5,vd1297)
| vd1306 = sK5
| sK4 = sK5
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| spl56_1279 ),
inference(resolution,[],[f24519,f23548]) ).
fof(f47285,plain,
( vd684 = vangle(sK4,sK5,vd1306)
| ~ ron(sK5,vd1297)
| vd1306 = sK5
| sK4 = sK5
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| spl56_1279 ),
inference(forward_subsumption_resolution,[],[f47284,f786]) ).
fof(f47287,plain,
( vd684 = vangle(sK4,sK5,vd1306)
| vd1306 = sK5
| sK4 = sK5
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| spl56_1279
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f47285,f25079]) ).
fof(f47289,plain,
( vd684 = vangle(sK4,sK5,vd1306)
| sK4 = sK5
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| spl56_39
| spl56_1279
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f47287,f2490]) ).
fof(f47291,plain,
( vd684 = vangle(sK4,sK5,vd1306)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| spl56_39
| spl56_1279
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f47289,f760]) ).
fof(f47293,plain,
( vd684 = vangle(sK4,sK5,vd1306)
| ~ rpoint(sK5)
| spl56_39
| spl56_1279
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f47291,f479]) ).
fof(f47295,plain,
( vd684 = vangle(sK4,sK5,vd1306)
| spl56_39
| spl56_1279
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f47293,f477]) ).
fof(f47297,plain,
( vd684 = sF52
| spl56_39
| spl56_1279
| ~ spl56_1362 ),
inference(forward_demodulation,[],[f47295,f1629]) ).
fof(f47299,plain,
( $false
| spl56_39
| spl56_1279
| spl56_1280
| ~ spl56_1362 ),
inference(forward_subsumption_resolution,[],[f47297,f24523]) ).
fof(f47300,plain,
( spl56_39
| spl56_1279
| spl56_1280
| ~ spl56_1362 ),
inference(avatar_contradiction_clause,[],[f47299]) ).
fof(f47301,plain,
( sF54 = vplus(vd684,vd684)
| ~ spl56_1280
| ~ spl56_1283 ),
inference(superposition,[],[f46783,f24522]) ).
fof(f47305,plain,
( vd684 = sF54
| ~ spl56_1280
| ~ spl56_1283 ),
inference(forward_demodulation,[],[f47301,f12346]) ).
fof(f47307,plain,
( $false
| ~ spl56_1280
| ~ spl56_1283
| ~ spl56_1285 ),
inference(forward_subsumption_resolution,[],[f47305,f46925]) ).
fof(f47308,plain,
( ~ spl56_1280
| ~ spl56_1283
| ~ spl56_1285 ),
inference(avatar_contradiction_clause,[],[f47307]) ).
fof(f47559,plain,
( ~ ron(vd1306,vd1297)
| vangle(sK4,sK6,sK5) = vangle(vd1306,sK6,sK5)
| ~ rpoint(vd1306)
| spl56_1328 ),
inference(forward_subsumption_resolution,[],[f36003,f793]) ).
fof(f47746,plain,
( vangle(sK4,sK6,sK5) = vangle(vd1306,sK6,sK5)
| ~ rpoint(vd1306)
| spl56_1328 ),
inference(forward_subsumption_resolution,[],[f47559,f543]) ).
fof(f47869,plain,
( vangle(sK4,sK6,sK5) = vangle(vd1306,sK6,sK5)
| spl56_1328 ),
inference(forward_subsumption_resolution,[],[f47746,f474]) ).
fof(f47942,plain,
( vangle(sK5,sK6,sK5) = vangle(sK4,sK6,sK5)
| ~ spl56_39
| spl56_1328 ),
inference(forward_demodulation,[],[f47869,f2491]) ).
fof(f47972,plain,
( vd684 = vangle(sK4,sK6,sK5)
| ~ spl56_39
| spl56_1328 ),
inference(forward_demodulation,[],[f47942,f2218]) ).
fof(f47980,plain,
( $false
| ~ spl56_39
| spl56_1305
| spl56_1328 ),
inference(forward_subsumption_resolution,[],[f47972,f24639]) ).
fof(f47981,plain,
( ~ spl56_39
| spl56_1305
| spl56_1328 ),
inference(avatar_contradiction_clause,[],[f47980]) ).
cnf(s15,plain,
( spl56_15
| ~ spl56_16 ),
inference(sat_conversion,[],[f1814]) ).
cnf(s38,plain,
( spl56_30
| spl56_41 ),
inference(sat_conversion,[],[f2505]) ).
cnf(s48,plain,
~ spl56_15,
inference(sat_conversion,[],[f2577]) ).
cnf(s51,plain,
( spl56_16
| ~ spl56_30 ),
inference(sat_conversion,[],[f2615]) ).
cnf(s771,plain,
( ~ spl56_13
| spl56_39 ),
inference(sat_conversion,[],[f14900]) ).
cnf(s1358,plain,
( ~ spl56_1283
| spl56_1286 ),
inference(sat_conversion,[],[f24554]) ).
cnf(s1368,plain,
( ~ spl56_1283
| spl56_1295 ),
inference(sat_conversion,[],[f24616]) ).
cnf(s1390,plain,
( ~ spl56_41
| spl56_1289
| ~ spl56_1328
| ~ spl56_1329 ),
inference(sat_conversion,[],[f24748]) ).
cnf(s1401,plain,
( spl56_13
| spl56_15
| ~ spl56_1340
| spl56_1341
| ~ spl56_1342 ),
inference(sat_conversion,[],[f24811]) ).
cnf(s1448,plain,
spl56_1329,
inference(sat_conversion,[],[f26422]) ).
cnf(s1465,plain,
( ~ spl56_1284
| ~ spl56_1334 ),
inference(sat_conversion,[],[f27991]) ).
cnf(s1472,plain,
( ~ spl56_1282
| ~ spl56_1370 ),
inference(sat_conversion,[],[f28073]) ).
cnf(s1473,plain,
( ~ spl56_1282
| spl56_1306 ),
inference(sat_conversion,[],[f28086]) ).
cnf(s1475,plain,
( ~ spl56_1282
| spl56_1286 ),
inference(sat_conversion,[],[f28089]) ).
cnf(s1476,plain,
( ~ spl56_1286
| spl56_1362 ),
inference(sat_conversion,[],[f28094]) ).
cnf(s1488,plain,
( spl56_1302
| ~ spl56_1342 ),
inference(sat_conversion,[],[f28690]) ).
cnf(s1492,plain,
( spl56_1281
| ~ spl56_1305
| ~ spl56_1394 ),
inference(sat_conversion,[],[f28750]) ).
cnf(s1507,plain,
( spl56_1304
| ~ spl56_1394 ),
inference(sat_conversion,[],[f30807]) ).
cnf(s1510,plain,
( ~ spl56_1304
| spl56_1342 ),
inference(sat_conversion,[],[f30922]) ).
cnf(s1576,plain,
~ spl56_1281,
inference(sat_conversion,[],[f31394]) ).
cnf(s1578,plain,
( ~ spl56_1278
| ~ spl56_1362 ),
inference(sat_conversion,[],[f31411]) ).
cnf(s1579,plain,
~ spl56_1303,
inference(sat_conversion,[],[f31535]) ).
cnf(s1581,plain,
( ~ spl56_1300
| ~ spl56_1369 ),
inference(sat_conversion,[],[f31690]) ).
cnf(s1582,plain,
( spl56_1300
| ~ spl56_1302
| ~ spl56_1341 ),
inference(sat_conversion,[],[f31692]) ).
cnf(s1602,plain,
( spl56_13
| spl56_1284
| spl56_1285 ),
inference(sat_conversion,[],[f32914]) ).
cnf(s1609,plain,
~ spl56_1289,
inference(sat_conversion,[],[f33056]) ).
cnf(s1631,plain,
( ~ spl56_1286
| ~ spl56_1362
| spl56_1422 ),
inference(sat_conversion,[],[f35575]) ).
cnf(s1642,plain,
( ~ spl56_1286
| spl56_1403
| ~ spl56_1422 ),
inference(sat_conversion,[],[f37960]) ).
cnf(s1645,plain,
( ~ spl56_1279
| ~ spl56_1339 ),
inference(sat_conversion,[],[f38579]) ).
cnf(s1648,plain,
( spl56_13
| spl56_30
| spl56_39
| spl56_1339
| spl56_1340
| ~ spl56_1362 ),
inference(sat_conversion,[],[f38659]) ).
cnf(s1696,plain,
( spl56_1278
| ~ spl56_1295
| spl56_1394 ),
inference(sat_conversion,[],[f42051]) ).
cnf(s1781,plain,
( spl56_1303
| ~ spl56_1306
| spl56_1394 ),
inference(sat_conversion,[],[f43365]) ).
cnf(s1787,plain,
( spl56_1282
| spl56_1283 ),
inference(sat_conversion,[],[f43395]) ).
cnf(s1843,plain,
( spl56_1369
| ~ spl56_1403 ),
inference(sat_conversion,[],[f44086]) ).
cnf(s1919,plain,
( spl56_1305
| spl56_1334
| ~ spl56_1403 ),
inference(sat_conversion,[],[f45144]) ).
cnf(s1940,plain,
( spl56_1305
| spl56_1370
| ~ spl56_1403 ),
inference(sat_conversion,[],[f45523]) ).
cnf(s1999,plain,
( spl56_39
| spl56_1279
| spl56_1280
| ~ spl56_1362 ),
inference(sat_conversion,[],[f47300]) ).
cnf(s2000,plain,
( ~ spl56_1280
| ~ spl56_1283
| ~ spl56_1285 ),
inference(sat_conversion,[],[f47308]) ).
cnf(s2020,plain,
( ~ spl56_39
| spl56_1305
| spl56_1328 ),
inference(sat_conversion,[],[f47981]) ).
cnf(s2058,plain,
( ~ spl56_1305
| ~ spl56_1394 ),
inference(rat,[],[s1492,s1576]) ).
cnf(s2069,plain,
( ~ spl56_41
| ~ spl56_1328 ),
inference(rat,[],[s1390,s1448,s1609]) ).
cnf(s2234,plain,
~ spl56_16,
inference(rat,[],[s15,s48]) ).
cnf(s2235,plain,
~ spl56_30,
inference(rat,[],[s51,s2234]) ).
cnf(s2238,plain,
spl56_41,
inference(rat,[],[s38,s2235]) ).
cnf(s2242,plain,
~ spl56_1328,
inference(rat,[],[s2069,s2238]) ).
cnf(s2289,plain,
~ spl56_1282,
inference(rat,[],[s1940,s1642,s2058,s1631,s1781,s1476,s1472,s1473,s1475,s1579]) ).
cnf(s2290,plain,
spl56_1283,
inference(rat,[],[s1787,s2289]) ).
cnf(s2294,plain,
spl56_1295,
inference(rat,[],[s1368,s2290]) ).
cnf(s2295,plain,
spl56_1286,
inference(rat,[],[s1358,s2290]) ).
cnf(s2316,plain,
spl56_1362,
inference(rat,[],[s1476,s2295]) ).
cnf(s2318,plain,
spl56_1422,
inference(rat,[],[s1631,s2295,s2316]) ).
cnf(s2319,plain,
~ spl56_1278,
inference(rat,[],[s1578,s2316]) ).
cnf(s2322,plain,
spl56_1403,
inference(rat,[],[s1642,s2295,s2318]) ).
cnf(s2323,plain,
spl56_1394,
inference(rat,[],[s1696,s2294,s2319]) ).
cnf(s2327,plain,
spl56_1369,
inference(rat,[],[s1843,s2322]) ).
cnf(s2333,plain,
spl56_1304,
inference(rat,[],[s1507,s2323]) ).
cnf(s2334,plain,
~ spl56_1305,
inference(rat,[],[s2058,s2323]) ).
cnf(s2336,plain,
~ spl56_1300,
inference(rat,[],[s1581,s2327]) ).
cnf(s2337,plain,
spl56_1342,
inference(rat,[],[s1510,s2333]) ).
cnf(s2339,plain,
~ spl56_39,
inference(rat,[],[s2020,s2242,s2334]) ).
cnf(s2345,plain,
spl56_1334,
inference(rat,[],[s1919,s2322,s2334]) ).
cnf(s2349,plain,
spl56_1302,
inference(rat,[],[s1488,s2337]) ).
cnf(s2353,plain,
~ spl56_13,
inference(rat,[],[s771,s2339]) ).
cnf(s2365,plain,
~ spl56_1284,
inference(rat,[],[s1465,s2345]) ).
cnf(s2367,plain,
~ spl56_1341,
inference(rat,[],[s1582,s2336,s2349]) ).
cnf(s2382,plain,
spl56_1285,
inference(rat,[],[s1602,s2353,s2365]) ).
cnf(s2384,plain,
~ spl56_1340,
inference(rat,[],[s1401,s2337,s2353,s48,s2367]) ).
cnf(s2401,plain,
~ spl56_1280,
inference(rat,[],[s2000,s2290,s2382]) ).
cnf(s2403,plain,
spl56_1339,
inference(rat,[],[s1648,s2316,s2339,s2353,s2235,s2384]) ).
cnf(s2407,plain,
spl56_1279,
inference(rat,[],[s1999,s2316,s2339,s2401]) ).
cnf(s2410,plain,
$false,
inference(rat,[],[s1645,s2403,s2407]) ).
fof(f47990,plain,
$false,
inference(avatar_sat_refutation,[],[s2410]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO316+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.41 % Computer : n005.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sun Sep 27 08:04:17 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.47 Running first-order theorem proving
% 0.14/0.47 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.79/4.35 % (3664545)Detected formulas, will run a generic FOF schedule.
% 23.79/4.35 % (3664556)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=2592665227:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 23.79/4.35 % (3664561)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3582450557:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 23.79/4.35 % (3664560)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1421049645:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 23.79/4.35 % (3664558)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=4149708495:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 23.79/4.35 % (3664559)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1359571680:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 23.79/4.35 % (3664557)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=2402698140:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 23.79/4.35 % (3664562)dis-21_1_sil=8000:lcm=predicate:random_seed=3906958688: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)
% 23.79/4.35 % (3664560)Instruction limit reached!
% 23.79/4.35 % (3664560)------------------------------
% 23.79/4.35 % (3664560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.79/4.35 % (3664560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.79/4.35 % (3664560)CaDiCaL version: 2.1.3
% 23.79/4.35 % (3664560)Termination reason: Instruction limit
% 23.79/4.35 % (3664560)Termination phase: Saturation
% 23.79/4.35 % (3664560)Time elapsed: 0.095 s
% 23.79/4.35 % (3664560)Peak memory usage: 89 MB
% 23.79/4.35 % (3664560)Instructions burned: 119 (million)
% 23.79/4.35 % (3664559)Instruction limit reached!
% 23.79/4.35 % (3664559)------------------------------
% 23.79/4.35 % (3664559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.79/4.35 % (3664559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.79/4.35 % (3664559)CaDiCaL version: 2.1.3
% 23.79/4.35 % (3664559)Termination reason: Instruction limit
% 23.79/4.35 % (3664559)Termination phase: Saturation
% 23.79/4.35 % (3664559)Time elapsed: 0.099 s
% 23.79/4.35 % (3664559)Peak memory usage: 90 MB
% 23.79/4.35 % (3664559)Instructions burned: 110 (million)
% 23.79/4.35 % (3664561)Instruction limit reached!
% 23.79/4.35 % (3664561)------------------------------
% 23.79/4.35 % (3664561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.79/4.35 % (3664561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.79/4.35 % (3664561)CaDiCaL version: 2.1.3
% 23.79/4.35 % (3664561)Termination reason: Instruction limit
% 23.79/4.35 % (3664561)Termination phase: Saturation
% 23.79/4.35 % (3664561)Time elapsed: 0.129 s
% 23.79/4.35 % (3664561)Peak memory usage: 90 MB
% 23.79/4.35 % (3664561)Instructions burned: 139 (million)
% 23.79/4.35 % (3664562)Instruction limit reached!
% 23.79/4.35 % (3664562)------------------------------
% 23.79/4.35 % (3664562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.79/4.35 % (3664562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.79/4.35 % (3664562)CaDiCaL version: 2.1.3
% 23.79/4.35 % (3664562)Termination reason: Instruction limit
% 23.79/4.35 % (3664562)Termination phase: Saturation
% 23.79/4.35 % (3664562)Time elapsed: 0.116 s
% 23.79/4.35 % (3664562)Peak memory usage: 90 MB
% 23.79/4.35 % (3664562)Instructions burned: 129 (million)
% 23.79/4.35 % (3664571)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2732790859:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 23.79/4.35 % (3664572)lrs+1011_1_sil=32000:sp=occurrence:random_seed=652130767:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 23.79/4.35 % (3664570)lrs+10_1_sil=8000:sp=occurrence:random_seed=2003858931:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 23.79/4.35 % (3664573)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=3793795360:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 23.79/4.35 % (3664571)Instruction limit reached!
% 34.14/5.86 % (3664571)------------------------------
% 34.14/5.86 % (3664571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.14/5.86 % (3664571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.14/5.86 % (3664571)CaDiCaL version: 2.1.3
% 34.14/5.86 % (3664571)Termination reason: Instruction limit
% 34.14/5.86 % (3664571)Termination phase: Saturation
% 34.14/5.86 % (3664571)Time elapsed: 0.123 s
% 34.14/5.86 % (3664571)Peak memory usage: 89 MB
% 34.14/5.86 % (3664571)Instructions burned: 157 (million)
% 34.14/5.86 % (3664570)Instruction limit reached!
% 34.14/5.86 % (3664570)------------------------------
% 34.14/5.86 % (3664570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.14/5.86 % (3664570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.14/5.86 % (3664570)CaDiCaL version: 2.1.3
% 34.14/5.86 % (3664570)Termination reason: Instruction limit
% 34.14/5.86 % (3664570)Termination phase: Saturation
% 34.14/5.86 % (3664570)Time elapsed: 0.231 s
% 34.14/5.86 % (3664570)Peak memory usage: 91 MB
% 34.14/5.86 % (3664570)Instructions burned: 285 (million)
% 34.14/5.86 % (3664573)Instruction limit reached!
% 34.14/5.86 % (3664573)------------------------------
% 34.14/5.86 % (3664573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.14/5.86 % (3664573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.14/5.86 % (3664573)CaDiCaL version: 2.1.3
% 34.14/5.86 % (3664573)Termination reason: Instruction limit
% 34.14/5.86 % (3664573)Termination phase: Saturation
% 34.14/5.86 % (3664573)Time elapsed: 0.202 s
% 34.14/5.86 % (3664573)Peak memory usage: 90 MB
% 34.14/5.86 % (3664573)Instructions burned: 249 (million)
% 34.14/5.86 % (3664572)Instruction limit reached!
% 34.14/5.86 % (3664572)------------------------------
% 34.14/5.86 % (3664572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.14/5.86 % (3664572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.14/5.86 % (3664572)CaDiCaL version: 2.1.3
% 34.14/5.86 % (3664572)Termination reason: Instruction limit
% 34.14/5.86 % (3664572)Termination phase: Saturation
% 34.14/5.86 % (3664572)Time elapsed: 0.286 s
% 34.14/5.86 % (3664572)Peak memory usage: 91 MB
% 34.14/5.86 % (3664572)Instructions burned: 325 (million)
% 34.14/5.86 % (3664584)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=999042314:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 34.14/5.86 % (3664589)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2768582796:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 34.14/5.86 % (3664592)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2336675791:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 34.14/5.86 % (3664590)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=245138369:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 34.14/5.86 % (3664592)Refutation not found, incomplete strategy
% 34.14/5.86 % (3664592)------------------------------
% 34.14/5.86 % (3664592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.14/5.86 % (3664592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.14/5.86 % (3664592)CaDiCaL version: 2.1.3
% 34.14/5.86 % (3664592)Termination reason: Refutation not found, incomplete strategy
% 34.14/5.86 % (3664592)Time elapsed: 0.048 s
% 34.14/5.86 % (3664592)Peak memory usage: 89 MB
% 34.14/5.86 % (3664592)Instructions burned: 54 (million)
% 34.14/5.86 % (3664590)Instruction limit reached!
% 34.14/5.86 % (3664590)------------------------------
% 34.14/5.86 % (3664590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.14/5.86 % (3664590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.14/5.86 % (3664590)CaDiCaL version: 2.1.3
% 34.14/5.86 % (3664590)Termination reason: Instruction limit
% 34.14/5.86 % (3664590)Termination phase: Saturation
% 34.14/5.86 % (3664590)Time elapsed: 0.099 s
% 34.14/5.86 % (3664590)Peak memory usage: 90 MB
% 34.14/5.86 % (3664590)Instructions burned: 114 (million)
% 34.14/5.86 % (3664584)Instruction limit reached!
% 34.14/5.86 % (3664584)------------------------------
% 34.14/5.86 % (3664584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.14/5.86 % (3664584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.14/5.86 % (3664584)CaDiCaL version: 2.1.3
% 34.14/5.86 % (3664584)Termination reason: Instruction limit
% 34.14/5.86 % (3664584)Termination phase: Saturation
% 34.64/6.02 % (3664584)Time elapsed: 0.247 s
% 34.64/6.02 % (3664584)Peak memory usage: 89 MB
% 34.64/6.02 % (3664584)Instructions burned: 294 (million)
% 34.64/6.02 % (3664602)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2480125770:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 34.64/6.02 % (3664603)lrs+10_1_sil=8000:sp=occurrence:random_seed=1260212660:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 34.64/6.02 % (3664592)------------------------------
% 34.64/6.02 % (3664592)------------------------------
% 34.64/6.02 % (3664602)Instruction limit reached!
% 34.64/6.02 % (3664602)------------------------------
% 34.64/6.02 % (3664602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.64/6.02 % (3664602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.64/6.02 % (3664602)CaDiCaL version: 2.1.3
% 34.64/6.02 % (3664602)Termination reason: Instruction limit
% 34.64/6.02 % (3664602)Termination phase: Saturation
% 34.64/6.02 % (3664602)Time elapsed: 0.085 s
% 34.64/6.02 % (3664602)Peak memory usage: 89 MB
% 34.64/6.02 % (3664602)Instructions burned: 114 (million)
% 34.64/6.02 % (3664606)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3618399062:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 34.64/6.02 % (3664606)Refutation not found, incomplete strategy
% 34.64/6.02 % (3664606)------------------------------
% 34.64/6.02 % (3664606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.64/6.02 % (3664606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.64/6.02 % (3664606)CaDiCaL version: 2.1.3
% 34.64/6.02 % (3664606)Termination reason: Refutation not found, incomplete strategy
% 34.64/6.02 % (3664606)Time elapsed: 0.033 s
% 34.64/6.02 % (3664606)Peak memory usage: 89 MB
% 34.64/6.02 % (3664606)Instructions burned: 34 (million)
% 34.64/6.02 % (3664607)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3761760614:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 34.64/6.02 % (3664606)------------------------------
% 34.64/6.02 % (3664606)------------------------------
% 34.64/6.02 % (3664603)Instruction limit reached!
% 34.64/6.02 % (3664603)------------------------------
% 34.64/6.02 % (3664603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.64/6.02 % (3664603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.64/6.02 % (3664603)CaDiCaL version: 2.1.3
% 34.64/6.02 % (3664603)Termination reason: Instruction limit
% 34.64/6.02 % (3664603)Termination phase: Saturation
% 34.64/6.02 % (3664603)Time elapsed: 0.797 s
% 34.64/6.02 % (3664603)Peak memory usage: 96 MB
% 34.64/6.02 % (3664603)Instructions burned: 907 (million)
% 34.64/6.02 % (3664610)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=148369508:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2977 on theBenchmark for (2977ds/134Mi)
% 34.64/6.02 % (3664611)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2989348645:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi)
% 34.64/6.02 % (3664610)Instruction limit reached!
% 34.64/6.02 % (3664610)------------------------------
% 34.64/6.02 % (3664610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.64/6.02 % (3664610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.64/6.02 % (3664610)CaDiCaL version: 2.1.3
% 34.64/6.02 % (3664610)Termination reason: Instruction limit
% 34.64/6.02 % (3664610)Termination phase: Saturation
% 34.64/6.02 % (3664610)Time elapsed: 0.118 s
% 34.64/6.02 % (3664610)Peak memory usage: 93 MB
% 34.64/6.02 % (3664610)Instructions burned: 135 (million)
% 34.64/6.02 % (3664614)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1902013592:st=3:i=13193:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/13193Mi)
% 34.64/6.02 % (3664611)Instruction limit reached!
% 34.64/6.02 % (3664611)------------------------------
% 34.64/6.02 % (3664611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.64/6.02 % (3664611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.64/6.02 % (3664611)CaDiCaL version: 2.1.3
% 34.64/6.02 % (3664611)Termination reason: Instruction limit
% 34.64/6.02 % (3664611)Termination phase: Saturation
% 34.64/6.02 % (3664611)Time elapsed: 0.485 s
% 34.64/6.02 % (3664611)Peak memory usage: 92 MB
% 34.64/6.02 % (3664611)Instructions burned: 592 (million)
% 34.64/6.02 % (3664589)Instruction limit reached!
% 34.64/6.02 % (3664589)------------------------------
% 34.64/6.02 % (3664589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.64/6.02 % (3664589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.64/6.02 % (3664589)CaDiCaL version: 2.1.3
% 34.64/6.02 % (3664589)Termination reason: Instruction limit
% 34.64/6.02 % (3664589)Termination phase: Saturation
% 34.64/6.02 % (3664589)Time elapsed: 2.255 s
% 34.64/6.02 % (3664589)Peak memory usage: 141 MB
% 34.64/6.02 % (3664589)Instructions burned: 2350 (million)
% 34.64/6.02 % (3664616)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=2580523355:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/125Mi)
% 34.64/6.02 % (3664616)Refutation not found, incomplete strategy
% 34.64/6.02 % (3664616)------------------------------
% 34.64/6.02 % (3664616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.64/6.02 % (3664616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.64/6.02 % (3664616)CaDiCaL version: 2.1.3
% 34.64/6.02 % (3664616)Termination reason: Refutation not found, incomplete strategy
% 34.64/6.02 % (3664616)Time elapsed: 0.060 s
% 34.64/6.02 % (3664616)Peak memory usage: 90 MB
% 34.64/6.02 % (3664616)Instructions burned: 65 (million)
% 34.64/6.02 % (3664617)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1943162417:i=134:gtgl=5:slsql=off:gtg=exists_sym_2966 on theBenchmark for (2966ds/134Mi)
% 34.64/6.02 % (3664617)Instruction limit reached!
% 34.64/6.02 % (3664617)------------------------------
% 34.64/6.02 % (3664617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.64/6.02 % (3664617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.64/6.02 % (3664617)CaDiCaL version: 2.1.3
% 34.64/6.02 % (3664617)Termination reason: Instruction limit
% 34.64/6.02 % (3664617)Termination phase: Saturation
% 34.64/6.02 % (3664617)Time elapsed: 0.125 s
% 34.64/6.02 % (3664617)Peak memory usage: 91 MB
% 34.64/6.02 % (3664617)Instructions burned: 134 (million)
% 34.64/6.02 % (3664616)------------------------------
% 34.64/6.02 % (3664616)------------------------------
% 34.64/6.02 % (3664620)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1273942223:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/141Mi)
% 34.64/6.02 % (3664620)Refutation not found, incomplete strategy
% 34.64/6.02 % (3664620)------------------------------
% 34.64/6.02 % (3664620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.64/6.02 % (3664620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.64/6.02 % (3664620)CaDiCaL version: 2.1.3
% 34.64/6.02 % (3664620)Termination reason: Refutation not found, incomplete strategy
% 34.64/6.02 % (3664620)Time elapsed: 0.023 s
% 34.64/6.02 % (3664620)Peak memory usage: 88 MB
% 34.64/6.02 % (3664620)Instructions burned: 26 (million)
% 34.64/6.02 % (3664621)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2749829441:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2961 on theBenchmark for (2961ds/431Mi)
% 34.64/6.02 % (3664621)Refutation not found, incomplete strategy
% 34.64/6.02 % (3664621)------------------------------
% 34.64/6.02 % (3664621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.64/6.02 % (3664621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.64/6.02 % (3664621)CaDiCaL version: 2.1.3
% 34.64/6.02 % (3664621)Termination reason: Refutation not found, incomplete strategy
% 34.64/6.02 % (3664621)Time elapsed: 0.013 s
% 34.64/6.02 % (3664621)Peak memory usage: 89 MB
% 34.64/6.02 % (3664621)Instructions burned: 12 (million)
% 34.64/6.02 % (3664620)------------------------------
% 34.64/6.02 % (3664620)------------------------------
% 34.64/6.02 % (3664621)------------------------------
% 34.64/6.02 % (3664621)------------------------------
% 34.64/6.02 % (3664624)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=3297944115:i=6060:aac=none:ins=25_2954 on theBenchmark for (2954ds/6060Mi)
% 34.64/6.02 % (3664556)First to succeed.
% 34.64/6.02 % (3664556)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3664545"
% 34.64/6.02 % (3664625)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=3227158749:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2954 on theBenchmark for (2954ds/150Mi)
% 34.64/6.02 % (3664625)Instruction limit reached!
% 34.64/6.02 % (3664625)------------------------------
% 34.64/6.02 % (3664625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.64/6.02 % (3664625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.64/6.02 % (3664625)CaDiCaL version: 2.1.3
% 34.64/6.02 % (3664625)Termination reason: Instruction limit
% 34.64/6.02 % (3664625)Termination phase: Saturation
% 34.64/6.02 % (3664625)Time elapsed: 0.140 s
% 34.64/6.02 % (3664625)Peak memory usage: 92 MB
% 34.64/6.02 % (3664625)Instructions burned: 153 (million)
% 34.64/6.02 % (3664556)Refutation found. Thanks to Tanya!
% 34.64/6.02 % SZS status Theorem for theBenchmark
% 34.64/6.02 % SZS output start Proof for theBenchmark
% See solution above
% 36.42/6.29 % (3664556)------------------------------
% 36.42/6.29 % (3664556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.42/6.29 % (3664556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.42/6.29 % (3664556)CaDiCaL version: 2.1.3
% 36.42/6.29 % (3664556)Termination reason: Refutation
% 36.42/6.29 % (3664556)Time elapsed: 4.581 s
% 36.42/6.29 % (3664556)Peak memory usage: 177 MB
% 36.42/6.29 % (3664556)Instructions burned: 8663 (million)
% 36.42/6.29 % (3664556)------------------------------
% 36.42/6.29 % (3664556)------------------------------
% 36.42/6.29 % (3664545)Success in time 5.058 s
% 36.42/6.29 % Vampire exiting
%------------------------------------------------------------------------------