%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO311+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:52:25 AM UTC 2026
% Result : Theorem 44.34s 7.93s
% Output : Refutation 44.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 68
% Syntax : Number of formulae : 730 ( 121 unt; 27 def)
% Number of atoms : 4283 (1364 equ)
% Maximal formula atoms : 26 ( 5 avg)
% Number of connectives : 6179 (2626 ~;3324 |; 183 &)
% ( 31 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 26 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 17 con; 0-3 aty)
% Number of variables : 1348 ( 0 sgn1295 !; 53 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vangle(vd1287,vd1288,vd1306) = vangle(vd1287,vd1289,vd1299),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(conjunct2(359)), 1320, 0)') ).
fof(f2,negated_conjecture,
vangle(vd1287,vd1288,vd1306) != vangle(vd1287,vd1289,vd1299),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
vangle(vd1287,vd1299,vd1289) = vangle(vd1287,vd1306,vd1288),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(359)), 1319, 0)') ).
fof(f4,axiom,
vf(vd1299,vd1289) = vf(vd1306,vd1288),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(359), 1318, 0)') ).
fof(f5,axiom,
vangle(vd1288,vd1287,vd1289) = vangle(vd1299,vd1287,vd1289),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(358, 1317, 0)') ).
fof(f6,axiom,
vangle(vd1288,vd1287,vd1289) = vangle(vd1288,vd1287,vd1306),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(357, 1316, 0)') ).
fof(f7,axiom,
~ rR(vd1287,vd1289,vd1306),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','neg(neg(conjunct2(356)))') ).
fof(f9,axiom,
rR(vd1306,vd1287,vd1302),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(352), 1307, 0)') ).
fof(f10,axiom,
rpoint(vd1306),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(352, 0)') ).
fof(f11,axiom,
( vd1302 = vd1303
& rR(vd1289,vd1287,vd1302)
& rpoint(vd1303)
& rR(vd1288,vd1287,vd1299) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))') ).
fof(f12,axiom,
( vf(vd1287,vd1288) = vf(vd1287,vd1289)
& vd1288 != vd1289
& vd1287 != vd1289
& vd1287 != vd1288
& ? [X0] :
( vd1289 = X0
& rpoint(X0) )
& ? [X1] :
( vd1288 = X1
& rpoint(X1) )
& ? [X2] :
( vd1287 = X2
& rpoint(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))') ).
fof(f13,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( ~ rR(X0,X2,X4)
& ~ rR(X0,X1,X3)
& X4 != X0
& X3 != X0
& X2 != X0
& X1 != X0
& ron(X4,X6)
& ron(X2,X6)
& ron(X3,X5)
& ron(X1,X5)
& ron(X0,X5)
& ? [X7] :
( X6 = X7
& rline(X7) )
& ? [X8] :
( X5 = X8
& rline(X8) )
& ? [X9] :
( X4 = X9
& rpoint(X9) )
& ? [X10] :
( X3 = X10
& rpoint(X10) )
& ? [X11] :
( X2 = X11
& rpoint(X11) )
& ? [X12] :
( X1 = X12
& rpoint(X12) )
& ? [X13] :
( X0 = X13
& rpoint(X13) ) )
=> vangle(X1,X0,X2) = vangle(X3,X0,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))') ).
fof(f14,axiom,
! [X0,X1,X2,X3] :
( ( rR(X2,X1,X3)
& rR(X1,X0,X2)
& ? [X4] :
( X3 = X4
& rpoint(X4) )
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> rR(X1,X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(89), 0), imp(cond(axiom(89), 0)))') ).
fof(f15,axiom,
! [X0,X1,X2] :
( ( rR(X1,X0,X2)
& ? [X3] :
( X2 = X3
& rpoint(X3) )
& ? [X4] :
( X1 = X4
& rpoint(X4) )
& ? [X5] :
( X0 = X5
& rpoint(X5) ) )
=> ( ~ rR(X0,X1,X2)
& X0 != X2
& X0 != X1
& rR(X1,X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))') ).
fof(f17,axiom,
vd1299 = vd1300,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(348, 4)') ).
fof(f18,axiom,
rpoint(vd1300),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(348, 1)') ).
fof(f23,axiom,
vd1306 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(353)), 1309, 0)') ).
fof(f25,axiom,
vd1289 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(355)), 1313, 0)') ).
fof(f26,axiom,
vd1299 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(conjunct2(conjunct2(353))), 1311, 0)') ).
fof(f29,axiom,
ron(vd1302,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct2(349), 0)') ).
fof(f30,axiom,
vd1288 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(355), 1312, 0)') ).
fof(f35,axiom,
rline(vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(347, 0)') ).
fof(f38,axiom,
rline(vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(346, 0)') ).
fof(f45,axiom,
ron(vd1289,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(354))))), 0)') ).
fof(f46,axiom,
ron(vd1288,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(354))))), 0)') ).
fof(f47,axiom,
ron(vd1306,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(conjunct2(conjunct2(354)))), 0)') ).
fof(f48,axiom,
ron(vd1287,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(conjunct2(354))), 0)') ).
fof(f49,axiom,
ron(vd1299,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(354)), 0)') ).
fof(f50,axiom,
ron(vd1287,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(354), 0)') ).
fof(f55,axiom,
! [X0,X1] :
( ( X0 != X1
& ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ? [X4] :
( ron(X1,X4)
& ron(X0,X4)
& rline(X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(51), 0), imp(cond(axiom(51), 0)))') ).
fof(f60,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ron(X2,X6)
& ron(X0,X6)
& X0 != X4
& X0 != X2
& X6 = X7
& rline(X7)
& X4 = X5
& rpoint(X5)
& X2 = X3
& rpoint(X3)
& X0 = X1
& rpoint(X1) )
=> ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
<=> vangle(X2,X0,X4) = v0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(188), 0), imp(cond(axiom(188), 0)))') ).
fof(f63,axiom,
! [X0,X1,X2] :
( ( X0 != X2
& X0 != X1
& ? [X3] :
( X2 = X3
& rpoint(X3) )
& ? [X4] :
( X1 = X4
& rpoint(X4) )
& ? [X5] :
( X0 = X5
& rpoint(X5) ) )
=> vangle(X0,X1,X2) = vangle(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(168), 0), imp(cond(axiom(168), 0)))') ).
fof(f64,axiom,
! [X0,X1] :
( ( ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ( vf(X0,X1) = v0
<=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))') ).
fof(f69,axiom,
! [X0,X1,X2,X3] :
( ( rR(X3,X0,X1)
& rR(X1,X0,X2)
& ? [X4] :
( X3 = X4
& rpoint(X4) )
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> rR(X3,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(87), 0), imp(cond(axiom(87), 0)))') ).
fof(f71,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/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(73), 0), imp(cond(axiom(73), 0)))') ).
fof(f72,axiom,
! [X0,X1] :
( ( ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> vf(X0,X1) = vf(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(166), 0), imp(cond(axiom(166), 0)))') ).
fof(f76,axiom,
v0 = vd684,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(axiom(137), 2)') ).
fof(f82,axiom,
! [X0,X1] :
( rcenter(X0,X1)
=> rinside(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))') ).
fof(f83,axiom,
! [X0,X1] :
( ( X0 != X1
& ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ? [X4] :
( ron(X1,X4)
& rcenter(X0,X4)
& rcircle(X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(53), 0), imp(cond(axiom(53), 0)))') ).
fof(f97,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( X1 != X2
& ron(X2,X5)
& ron(X1,X5)
& rinside(X0,X5)
& ron(X2,X3)
& ron(X1,X3)
& ron(X0,X3)
& X5 = X6
& rcircle(X6)
& X3 = X4
& rline(X4)
& ? [X7] :
( X2 = X7
& rpoint(X7) )
& ? [X8] :
( X1 = X8
& rpoint(X8) )
& ? [X9] :
( X0 = X9
& rpoint(X9) ) )
=> rR(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(119), 0), imp(cond(axiom(119), 0)))') ).
fof(f107,axiom,
! [X0,X1,X2,X3] :
( ( rR(X1,X0,X3)
& rR(X1,X0,X2)
& ? [X4] :
( X3 = X4
& rpoint(X4) )
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ~ rR(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(93), 0), imp(cond(axiom(93), 0)))') ).
fof(f142,axiom,
! [X0,X1,X2,X3,X4] :
( ( vf(X2,X0) = vf(X2,X1)
& ron(X1,X4)
& ron(X0,X3)
& rcenter(X2,X4)
& rcenter(X2,X3)
& ? [X5] :
( X1 = X5
& rpoint(X5) )
& ? [X6] :
( X0 = X6
& rpoint(X6) ) )
=> X3 = X4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))') ).
fof(f152,plain,
vangle(vd1287,vd1288,vd1306) != vangle(vd1287,vd1289,vd1299),
inference(flattening,[],[f2]) ).
fof(f157,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,[],[f13]) ).
fof(f158,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,[],[f157]) ).
fof(f159,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,[],[f14]) ).
fof(f160,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,[],[f159]) ).
fof(f161,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,[],[f15]) ).
fof(f162,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,[],[f161]) ).
fof(f189,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,[],[f55]) ).
fof(f190,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,[],[f189]) ).
fof(f199,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,[],[f60]) ).
fof(f200,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,[],[f199]) ).
fof(f205,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,[],[f63]) ).
fof(f206,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,[],[f205]) ).
fof(f207,plain,
! [X0,X1] :
( ( vf(X0,X1) = v0
<=> X0 = X1 )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f64]) ).
fof(f208,plain,
! [X0,X1] :
( ( vf(X0,X1) = v0
<=> X0 = X1 )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f207]) ).
fof(f217,plain,
! [X0,X1,X2,X3] :
( rR(X3,X0,X2)
| ~ rR(X3,X0,X1)
| ~ rR(X1,X0,X2)
| ! [X4] :
( X3 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f69]) ).
fof(f218,plain,
! [X0,X1,X2,X3] :
( rR(X3,X0,X2)
| ~ rR(X3,X0,X1)
| ~ rR(X1,X0,X2)
| ! [X4] :
( X3 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f217]) ).
fof(f221,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,[],[f71]) ).
fof(f222,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,[],[f221]) ).
fof(f223,plain,
! [X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f72]) ).
fof(f224,plain,
! [X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f223]) ).
fof(f239,plain,
! [X0,X1] :
( rinside(X0,X1)
| ~ rcenter(X0,X1) ),
inference(ennf_transformation,[],[f82]) ).
fof(f240,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,[],[f83]) ).
fof(f241,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,[],[f240]) ).
fof(f267,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,[],[f97]) ).
fof(f268,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,[],[f267]) ).
fof(f287,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,[],[f107]) ).
fof(f288,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,[],[f287]) ).
fof(f353,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,[],[f142]) ).
fof(f354,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,[],[f353]) ).
fof(f369,plain,
( vf(vd1287,vd1288) = vf(vd1287,vd1289)
& vd1288 != vd1289
& vd1287 != vd1289
& vd1287 != vd1288
& vd1289 = sK1
& rpoint(sK1)
& vd1288 = sK2
& rpoint(sK2)
& vd1287 = sK3
& rpoint(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3)],[f12]) ).
fof(f378,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,[],[f190]) ).
fof(f379,plain,
! [X0,X1] :
( ( ron(X1,sK8(X0,X1))
& ron(X0,sK8(X0,X1))
& rline(sK8(X0,X1)) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X2,sK8(X0,X1))],[f378]) ).
fof(f382,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
| vangle(X2,X0,X4) != v0 )
& ( vangle(X2,X0,X4) = v0
| rR(X0,X2,X4)
| ~ ron(X4,X6) ) )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(nnf_transformation,[],[f200]) ).
fof(f383,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
| vangle(X2,X0,X4) != v0 )
& ( vangle(X2,X0,X4) = v0
| rR(X0,X2,X4)
| ~ ron(X4,X6) ) )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(flattening,[],[f382]) ).
fof(f386,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,[],[f208]) ).
fof(f392,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,[],[f241]) ).
fof(f393,plain,
! [X0,X1] :
( ( ron(X1,sK13(X0,X1))
& rcenter(X0,sK13(X0,X1))
& rcircle(sK13(X0,X1)) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X2,sK13(X0,X1))],[f392]) ).
fof(f445,plain,
vangle(vd1287,vd1288,vd1306) != vangle(vd1287,vd1289,vd1299),
inference(cnf_transformation,[],[f152]) ).
fof(f446,plain,
vangle(vd1287,vd1299,vd1289) = vangle(vd1287,vd1306,vd1288),
inference(cnf_transformation,[],[f3]) ).
fof(f447,plain,
vf(vd1299,vd1289) = vf(vd1306,vd1288),
inference(cnf_transformation,[],[f4]) ).
fof(f448,plain,
vangle(vd1288,vd1287,vd1289) = vangle(vd1299,vd1287,vd1289),
inference(cnf_transformation,[],[f5]) ).
fof(f449,plain,
vangle(vd1288,vd1287,vd1289) = vangle(vd1288,vd1287,vd1306),
inference(cnf_transformation,[],[f6]) ).
fof(f450,plain,
~ rR(vd1287,vd1289,vd1306),
inference(cnf_transformation,[],[f7]) ).
fof(f452,plain,
rR(vd1306,vd1287,vd1302),
inference(cnf_transformation,[],[f9]) ).
fof(f453,plain,
rpoint(vd1306),
inference(cnf_transformation,[],[f10]) ).
fof(f454,plain,
rR(vd1288,vd1287,vd1299),
inference(cnf_transformation,[],[f11]) ).
fof(f455,plain,
rpoint(vd1303),
inference(cnf_transformation,[],[f11]) ).
fof(f456,plain,
rR(vd1289,vd1287,vd1302),
inference(cnf_transformation,[],[f11]) ).
fof(f457,plain,
vd1302 = vd1303,
inference(cnf_transformation,[],[f11]) ).
fof(f458,plain,
rpoint(sK3),
inference(cnf_transformation,[],[f369]) ).
fof(f459,plain,
vd1287 = sK3,
inference(cnf_transformation,[],[f369]) ).
fof(f460,plain,
rpoint(sK2),
inference(cnf_transformation,[],[f369]) ).
fof(f461,plain,
vd1288 = sK2,
inference(cnf_transformation,[],[f369]) ).
fof(f462,plain,
rpoint(sK1),
inference(cnf_transformation,[],[f369]) ).
fof(f463,plain,
vd1289 = sK1,
inference(cnf_transformation,[],[f369]) ).
fof(f466,plain,
vd1288 != vd1289,
inference(cnf_transformation,[],[f369]) ).
fof(f467,plain,
vf(vd1287,vd1288) = vf(vd1287,vd1289),
inference(cnf_transformation,[],[f369]) ).
fof(f468,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,[],[f158]) ).
fof(f469,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,[],[f160]) ).
fof(f470,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,[],[f162]) ).
fof(f472,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,[],[f162]) ).
fof(f473,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,[],[f162]) ).
fof(f475,plain,
vd1299 = vd1300,
inference(cnf_transformation,[],[f17]) ).
fof(f476,plain,
rpoint(vd1300),
inference(cnf_transformation,[],[f18]) ).
fof(f490,plain,
vd1287 != vd1306,
inference(cnf_transformation,[],[f23]) ).
fof(f492,plain,
vd1287 != vd1289,
inference(cnf_transformation,[],[f25]) ).
fof(f493,plain,
vd1287 != vd1299,
inference(cnf_transformation,[],[f26]) ).
fof(f496,plain,
ron(vd1302,vd1297),
inference(cnf_transformation,[],[f29]) ).
fof(f497,plain,
vd1287 != vd1288,
inference(cnf_transformation,[],[f30]) ).
fof(f502,plain,
rline(vd1297),
inference(cnf_transformation,[],[f35]) ).
fof(f505,plain,
rline(vd1295),
inference(cnf_transformation,[],[f38]) ).
fof(f513,plain,
ron(vd1289,vd1297),
inference(cnf_transformation,[],[f45]) ).
fof(f514,plain,
ron(vd1288,vd1295),
inference(cnf_transformation,[],[f46]) ).
fof(f515,plain,
ron(vd1306,vd1297),
inference(cnf_transformation,[],[f47]) ).
fof(f516,plain,
ron(vd1287,vd1297),
inference(cnf_transformation,[],[f48]) ).
fof(f517,plain,
ron(vd1299,vd1295),
inference(cnf_transformation,[],[f49]) ).
fof(f518,plain,
ron(vd1287,vd1295),
inference(cnf_transformation,[],[f50]) ).
fof(f524,plain,
! [X3,X0,X1,X4] :
( rline(sK8(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f379]) ).
fof(f525,plain,
! [X3,X0,X1,X4] :
( ron(X0,sK8(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f379]) ).
fof(f526,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK8(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f379]) ).
fof(f533,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( vangle(X2,X0,X4) = v0
| rR(X0,X2,X4)
| ~ ron(X4,X6)
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f383]) ).
fof(f534,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X4,X6)
| vangle(X2,X0,X4) != v0
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f383]) ).
fof(f535,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rR(X0,X2,X4)
| vangle(X2,X0,X4) != v0
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f383]) ).
fof(f540,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,[],[f206]) ).
fof(f541,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| vf(X0,X1) != v0
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f386]) ).
fof(f542,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = v0
| X0 != X1
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f386]) ).
fof(f547,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( rR(X3,X0,X2)
| ~ rR(X3,X0,X1)
| ~ rR(X1,X0,X2)
| X3 != X4
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f218]) ).
fof(f549,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,[],[f222]) ).
fof(f550,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f224]) ).
fof(f554,plain,
v0 = vd684,
inference(cnf_transformation,[],[f76]) ).
fof(f578,plain,
! [X0,X1] :
( ~ rcenter(X0,X1)
| rinside(X0,X1) ),
inference(cnf_transformation,[],[f239]) ).
fof(f579,plain,
! [X3,X0,X1,X4] :
( rcircle(sK13(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f393]) ).
fof(f580,plain,
! [X3,X0,X1,X4] :
( rcenter(X0,sK13(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f393]) ).
fof(f581,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK13(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f393]) ).
fof(f609,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,[],[f268]) ).
fof(f619,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,[],[f288]) ).
fof(f728,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,[],[f354]) ).
fof(f739,plain,
vangle(sK3,sK2,vd1306) != vangle(sK3,sK1,vd1300),
inference(definition_unfolding,[],[f445,f459,f461,f459,f463,f475]) ).
fof(f740,plain,
vangle(sK3,vd1300,sK1) = vangle(sK3,vd1306,sK2),
inference(definition_unfolding,[],[f446,f459,f475,f463,f459,f461]) ).
fof(f741,plain,
vf(vd1300,sK1) = vf(vd1306,sK2),
inference(definition_unfolding,[],[f447,f475,f463,f461]) ).
fof(f742,plain,
vangle(sK2,sK3,sK1) = vangle(vd1300,sK3,sK1),
inference(definition_unfolding,[],[f448,f461,f459,f463,f475,f459,f463]) ).
fof(f743,plain,
vangle(sK2,sK3,sK1) = vangle(sK2,sK3,vd1306),
inference(definition_unfolding,[],[f449,f461,f459,f463,f461,f459]) ).
fof(f744,plain,
~ rR(sK3,sK1,vd1306),
inference(definition_unfolding,[],[f450,f459,f463]) ).
fof(f746,plain,
rR(vd1306,sK3,vd1303),
inference(definition_unfolding,[],[f452,f459,f457]) ).
fof(f747,plain,
rR(sK1,sK3,vd1303),
inference(definition_unfolding,[],[f456,f463,f459,f457]) ).
fof(f748,plain,
rR(sK2,sK3,vd1300),
inference(definition_unfolding,[],[f454,f461,f459,f475]) ).
fof(f749,plain,
vf(sK3,sK2) = vf(sK3,sK1),
inference(definition_unfolding,[],[f467,f459,f461,f459,f463]) ).
fof(f750,plain,
sK1 != sK2,
inference(definition_unfolding,[],[f466,f461,f463]) ).
fof(f755,plain,
vd1306 != sK3,
inference(definition_unfolding,[],[f490,f459]) ).
fof(f757,plain,
sK1 != sK3,
inference(definition_unfolding,[],[f492,f459,f463]) ).
fof(f758,plain,
vd1300 != sK3,
inference(definition_unfolding,[],[f493,f459,f475]) ).
fof(f760,plain,
ron(vd1303,vd1297),
inference(definition_unfolding,[],[f496,f457]) ).
fof(f761,plain,
sK2 != sK3,
inference(definition_unfolding,[],[f497,f459,f461]) ).
fof(f768,plain,
ron(sK1,vd1297),
inference(definition_unfolding,[],[f513,f463]) ).
fof(f769,plain,
ron(sK2,vd1295),
inference(definition_unfolding,[],[f514,f461]) ).
fof(f770,plain,
ron(sK3,vd1297),
inference(definition_unfolding,[],[f516,f459]) ).
fof(f771,plain,
ron(vd1300,vd1295),
inference(definition_unfolding,[],[f517,f475]) ).
fof(f772,plain,
ron(sK3,vd1295),
inference(definition_unfolding,[],[f518,f459]) ).
fof(f773,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,[],[f535,f554]) ).
fof(f774,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,[],[f534,f554]) ).
fof(f775,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,[],[f533,f554]) ).
fof(f776,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = vd684
| X0 != X1
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(definition_unfolding,[],[f542,f554]) ).
fof(f777,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| vf(X0,X1) != vd684
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(definition_unfolding,[],[f541,f554]) ).
fof(f782,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,[],[f468]) ).
fof(f783,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,[],[f782]) ).
fof(f784,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,[],[f783]) ).
fof(f785,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,[],[f784]) ).
fof(f786,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,[],[f785]) ).
fof(f787,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,[],[f786]) ).
fof(f788,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,[],[f787]) ).
fof(f789,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,[],[f469]) ).
fof(f790,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,[],[f789]) ).
fof(f791,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,[],[f790]) ).
fof(f792,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,[],[f791]) ).
fof(f793,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,[],[f473]) ).
fof(f794,plain,
! [X3,X0,X4,X5] :
( ~ rR(X0,X4,X3)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f793]) ).
fof(f795,plain,
! [X3,X4,X5] :
( ~ rR(X5,X4,X3)
| ~ rR(X4,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f794]) ).
fof(f796,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,[],[f472]) ).
fof(f797,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X3,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f796]) ).
fof(f798,plain,
! [X3,X4,X5] :
( ~ rR(X4,X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f797]) ).
fof(f799,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f798]) ).
fof(f804,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,[],[f470]) ).
fof(f805,plain,
! [X3,X0,X4,X5] :
( rR(X4,X3,X0)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f804]) ).
fof(f806,plain,
! [X3,X4,X5] :
( ~ rR(X4,X5,X3)
| rR(X4,X3,X5)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f805]) ).
fof(f920,plain,
! [X3,X0,X4] :
( ron(X3,sK8(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f526]) ).
fof(f921,plain,
! [X3,X4] :
( ron(X3,sK8(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f920]) ).
fof(f922,plain,
! [X3,X0,X4] :
( ron(X0,sK8(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f525]) ).
fof(f923,plain,
! [X3,X4] :
( ron(X4,sK8(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f922]) ).
fof(f924,plain,
! [X3,X0,X4] :
( rline(sK8(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f524]) ).
fof(f925,plain,
! [X3,X4] :
( rline(sK8(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f924]) ).
fof(f950,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,[],[f773]) ).
fof(f951,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,[],[f950]) ).
fof(f952,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,[],[f951]) ).
fof(f953,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,[],[f952]) ).
fof(f954,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,[],[f774]) ).
fof(f955,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,[],[f954]) ).
fof(f956,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,[],[f955]) ).
fof(f957,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,[],[f956]) ).
fof(f958,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,[],[f775]) ).
fof(f959,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,[],[f958]) ).
fof(f960,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,[],[f959]) ).
fof(f961,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,[],[f960]) ).
fof(f970,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,[],[f540]) ).
fof(f971,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,[],[f970]) ).
fof(f972,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,[],[f971]) ).
fof(f973,plain,
! [X2,X3,X1] :
( vd684 = vf(X1,X1)
| X1 != X2
| ~ rpoint(X2)
| X1 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f776]) ).
fof(f974,plain,
! [X2,X3] :
( vd684 = vf(X2,X2)
| ~ rpoint(X2)
| X2 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f973]) ).
fof(f975,plain,
! [X3] :
( vd684 = vf(X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f974]) ).
fof(f976,plain,
! [X2,X3,X0] :
( X0 = X2
| vf(X0,X2) != vd684
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f777]) ).
fof(f977,plain,
! [X2,X3] :
( vd684 != vf(X3,X2)
| X2 = X3
| ~ rpoint(X2)
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f976]) ).
fof(f990,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( rR(X4,X0,X2)
| ~ rR(X4,X0,X1)
| ~ rR(X1,X0,X2)
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f547]) ).
fof(f991,plain,
! [X0,X1,X6,X7,X4,X5] :
( rR(X4,X0,X5)
| ~ rR(X4,X0,X1)
| ~ rR(X1,X0,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f990]) ).
fof(f992,plain,
! [X0,X6,X7,X4,X5] :
( rR(X4,X0,X5)
| ~ rR(X4,X0,X6)
| ~ rR(X6,X0,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f991]) ).
fof(f993,plain,
! [X6,X7,X4,X5] :
( ~ rR(X6,X7,X5)
| ~ rR(X4,X7,X6)
| rR(X4,X7,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f992]) ).
fof(f996,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,[],[f549]) ).
fof(f997,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,[],[f996]) ).
fof(f998,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,[],[f997]) ).
fof(f999,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,[],[f998]) ).
fof(f1000,plain,
! [X2,X3,X0] :
( vf(X0,X2) = vf(X2,X0)
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f550]) ).
fof(f1001,plain,
! [X2,X3] :
( ~ rpoint(X3)
| ~ rpoint(X2)
| vf(X3,X2) = vf(X2,X3) ),
inference(equality_resolution,[],[f1000]) ).
fof(f1065,plain,
! [X3,X0,X4] :
( ron(X3,sK13(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f581]) ).
fof(f1066,plain,
! [X3,X4] :
( ron(X3,sK13(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1065]) ).
fof(f1067,plain,
! [X3,X0,X4] :
( rcenter(X0,sK13(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f580]) ).
fof(f1068,plain,
! [X3,X4] :
( rcenter(X4,sK13(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1067]) ).
fof(f1069,plain,
! [X3,X0,X4] :
( rcircle(sK13(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f579]) ).
fof(f1070,plain,
! [X3,X4] :
( rcircle(sK13(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1069]) ).
fof(f1157,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,[],[f609]) ).
fof(f1158,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,[],[f1157]) ).
fof(f1159,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,[],[f1158]) ).
fof(f1160,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,[],[f1159]) ).
fof(f1161,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,[],[f1160]) ).
fof(f1206,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,[],[f619]) ).
fof(f1207,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,[],[f1206]) ).
fof(f1208,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,[],[f1207]) ).
fof(f1209,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,[],[f1208]) ).
fof(f1506,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,[],[f728]) ).
fof(f1507,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,[],[f1506]) ).
fof(f1552,definition,
sF52 = vangle(sK3,sK2,vd1306),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f1553,plain,
vangle(sK3,sK2,vd1306) = sF52,
inference(reorient_equations,[],[f1552]) ).
fof(f1554,definition,
sF53 = vangle(sK3,sK1,vd1300),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f1555,plain,
vangle(sK3,sK1,vd1300) = sF53,
inference(reorient_equations,[],[f1554]) ).
fof(f1556,plain,
sF52 != sF53,
inference(definition_folding,[],[f739,f1555,f1553]) ).
fof(f1557,plain,
! [X3] :
( ~ rpoint(X3)
| vd684 = vf(X3,X3) ),
inference(duplicate_literal_removal,[],[f975]) ).
fof(f1559,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f799]) ).
fof(f1607,plain,
( rR(sK2,vd1300,sK3)
| ~ rpoint(vd1300)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(resolution,[],[f806,f748]) ).
fof(f1608,plain,
( rR(sK1,vd1303,sK3)
| ~ rpoint(vd1303)
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(resolution,[],[f806,f747]) ).
fof(f1609,plain,
( rR(sK1,vd1303,sK3)
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1608,f455]) ).
fof(f1610,plain,
( rR(sK2,vd1300,sK3)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1607,f476]) ).
fof(f1611,plain,
( rR(sK1,vd1303,sK3)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1609,f462]) ).
fof(f1612,plain,
( rR(sK2,vd1300,sK3)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1610,f460]) ).
fof(f1613,plain,
rR(sK1,vd1303,sK3),
inference(forward_subsumption_resolution,[],[f1611,f458]) ).
fof(f1614,plain,
rR(sK2,vd1300,sK3),
inference(forward_subsumption_resolution,[],[f1612,f458]) ).
fof(f1619,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK3,X0,X1)
| rR(sK3,X2,X3)
| sK3 = X1
| sK3 = X3
| sK3 = X0
| sK3 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1295)
| ~ ron(X2,vd1295)
| vangle(X3,sK3,X1) = vangle(X2,sK3,X0)
| ~ rline(X4)
| ~ rline(vd1295)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK3) ),
inference(resolution,[],[f788,f772]) ).
fof(f1620,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK2,X0,X1)
| rR(sK2,X2,X3)
| sK2 = X1
| sK2 = X3
| sK2 = X0
| sK2 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1295)
| ~ ron(X2,vd1295)
| vangle(X3,sK2,X1) = vangle(X2,sK2,X0)
| ~ rline(X4)
| ~ rline(vd1295)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK2) ),
inference(resolution,[],[f788,f769]) ).
fof(f1623,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK3,X0,X1)
| rR(sK3,X2,X3)
| sK3 = X1
| sK3 = X3
| sK3 = X0
| sK3 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK3,X1) = vangle(X2,sK3,X0)
| ~ rline(X4)
| ~ rline(vd1297)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK3) ),
inference(resolution,[],[f770,f788]) ).
fof(f1625,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK1,X0,X1)
| rR(sK1,X2,X3)
| sK1 = X1
| sK1 = X3
| sK1 = X0
| sK1 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK1,X1) = vangle(X2,sK1,X0)
| ~ rline(X4)
| ~ rline(vd1297)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK1) ),
inference(resolution,[],[f768,f788]) ).
fof(f1629,plain,
! [X0,X1] :
( ~ rpoint(X1)
| vd1300 = X1
| ~ rpoint(X0)
| vd1300 = X0
| vangle(X0,X1,vd1300) = vangle(vd1300,X1,X0) ),
inference(resolution,[],[f972,f476]) ).
fof(f1631,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK2 = X1
| ~ rpoint(X0)
| sK2 = X0
| vangle(X0,X1,sK2) = vangle(sK2,X1,X0) ),
inference(resolution,[],[f972,f460]) ).
fof(f1632,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK3 = X1
| ~ rpoint(X0)
| sK3 = X0
| vangle(X0,X1,sK3) = vangle(sK3,X1,X0) ),
inference(resolution,[],[f972,f458]) ).
fof(f1647,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,[],[f961,f515]) ).
fof(f1651,plain,
vd684 = vf(sK1,sK1),
inference(resolution,[],[f1557,f462]) ).
fof(f1652,plain,
vd684 = vf(sK2,sK2),
inference(resolution,[],[f1557,f460]) ).
fof(f1654,plain,
! [X0,X1] :
( rR(X0,X1,vd1303)
| vd684 = vangle(X1,X0,vd1303)
| ~ ron(X1,vd1297)
| ~ ron(X0,vd1297)
| vd1303 = X0
| X0 = X1
| ~ rline(vd1297)
| ~ rpoint(vd1303)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f760,f961]) ).
fof(f1657,plain,
( ~ rR(sK3,sK1,vd1303)
| ~ rpoint(vd1303)
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(resolution,[],[f795,f747]) ).
fof(f1666,plain,
( ~ rR(sK3,sK1,vd1303)
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f1657,f455]) ).
fof(f1671,plain,
( ~ rR(sK3,sK1,vd1303)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f1666,f458]) ).
fof(f1676,plain,
~ rR(sK3,sK1,vd1303),
inference(forward_subsumption_resolution,[],[f1671,f462]) ).
fof(f1677,plain,
! [X0,X1] :
( ~ ron(X0,X1)
| ~ ron(X0,vd1295)
| ~ ron(sK3,X1)
| vd1295 = X1
| ~ rline(X1)
| ~ rline(vd1295)
| sK3 = X0
| ~ rpoint(X0)
| ~ rpoint(sK3) ),
inference(resolution,[],[f999,f772]) ).
fof(f1691,plain,
! [X0] :
( ~ rR(X0,sK3,vd1306)
| rR(X0,sK3,vd1303)
| ~ rpoint(X0)
| ~ rpoint(vd1303)
| ~ rpoint(vd1306)
| ~ rpoint(sK3) ),
inference(resolution,[],[f993,f746]) ).
fof(f1698,plain,
! [X0] :
( ~ rR(X0,sK3,vd1306)
| rR(X0,sK3,vd1303)
| ~ rpoint(X0)
| ~ rpoint(vd1306)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1691,f455]) ).
fof(f1704,plain,
! [X0] :
( ~ rR(X0,sK3,vd1306)
| rR(X0,sK3,vd1303)
| ~ rpoint(X0)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1698,f453]) ).
fof(f1710,plain,
! [X0] :
( ~ rR(X0,sK3,vd1306)
| rR(X0,sK3,vd1303)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1704,f458]) ).
fof(f1713,plain,
! [X0] :
( ~ rpoint(X0)
| vf(vd1306,X0) = vf(X0,vd1306) ),
inference(resolution,[],[f1001,f453]) ).
fof(f1715,plain,
! [X0] :
( ~ rpoint(X0)
| vf(vd1300,X0) = vf(X0,vd1300) ),
inference(resolution,[],[f1001,f476]) ).
fof(f1722,plain,
! [X0] :
( ~ rR(sK3,sK2,X0)
| rR(sK2,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rpoint(vd1300) ),
inference(resolution,[],[f792,f1614]) ).
fof(f1723,plain,
! [X0] :
( ~ rR(sK3,sK1,X0)
| rR(sK1,vd1303,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ rpoint(vd1303) ),
inference(resolution,[],[f792,f1613]) ).
fof(f1726,plain,
! [X0] :
( ~ rR(sK3,sK1,X0)
| rR(sK1,vd1303,X0)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(vd1303) ),
inference(forward_subsumption_resolution,[],[f1723,f458]) ).
fof(f1727,plain,
! [X0] :
( ~ rR(sK3,sK2,X0)
| rR(sK2,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(sK2)
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f1722,f458]) ).
fof(f1732,plain,
! [X0] :
( ~ rR(sK3,sK1,X0)
| rR(sK1,vd1303,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1303) ),
inference(forward_subsumption_resolution,[],[f1726,f462]) ).
fof(f1733,plain,
! [X0] :
( ~ rR(sK3,sK2,X0)
| rR(sK2,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f1727,f460]) ).
fof(f1738,plain,
! [X0] :
( ~ rR(sK3,sK1,X0)
| rR(sK1,vd1303,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1732,f455]) ).
fof(f1739,plain,
! [X0] :
( ~ rR(sK3,sK2,X0)
| rR(sK2,vd1300,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1733,f476]) ).
fof(f1747,definition,
( spl54_13
<=> vd1306 = sK2 ),
introduced(definition,[new_symbols(definition,[spl54_13])],[avatar_definition]) ).
fof(f1748,plain,
( vd1306 != sK2
| spl54_13 ),
inference(avatar_component_clause,[],[f1747]) ).
fof(f1749,plain,
( vd1306 = sK2
| ~ spl54_13 ),
inference(avatar_component_clause,[],[f1747]) ).
fof(f1764,plain,
vf(vd1306,sK2) = vf(sK2,vd1306),
inference(resolution,[],[f1713,f460]) ).
fof(f1767,plain,
vf(vd1300,sK1) = vf(sK2,vd1306),
inference(forward_demodulation,[],[f1764,f741]) ).
fof(f1768,plain,
( vd684 != vf(sK2,vd1306)
| vd1300 = sK1
| ~ rpoint(sK1)
| ~ rpoint(vd1300) ),
inference(superposition,[],[f977,f1767]) ).
fof(f1769,plain,
( vd684 != vf(sK2,vd1306)
| vd1300 = sK1
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f1768,f462]) ).
fof(f1770,plain,
( vd684 != vf(sK2,vd1306)
| vd1300 = sK1 ),
inference(forward_subsumption_resolution,[],[f1769,f476]) ).
fof(f1772,definition,
( spl54_15
<=> vd1300 = sK1 ),
introduced(definition,[new_symbols(definition,[spl54_15])],[avatar_definition]) ).
fof(f1773,plain,
( vd1300 != sK1
| spl54_15 ),
inference(avatar_component_clause,[],[f1772]) ).
fof(f1774,plain,
( vd1300 = sK1
| ~ spl54_15 ),
inference(avatar_component_clause,[],[f1772]) ).
fof(f1776,definition,
( spl54_16
<=> vd684 = vf(sK2,vd1306) ),
introduced(definition,[new_symbols(definition,[spl54_16])],[avatar_definition]) ).
fof(f1778,plain,
( vd684 != vf(sK2,vd1306)
| spl54_16 ),
inference(avatar_component_clause,[],[f1776]) ).
fof(f1779,plain,
( spl54_15
| ~ spl54_16 ),
inference(avatar_split_clause,[],[f1770,f1776,f1772]) ).
fof(f1781,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X0)
| vd684 = vangle(X3,X2,X0)
| ~ ron(X3,sK8(X1,X0))
| ~ ron(X2,sK8(X1,X0))
| X0 = X2
| X2 = X3
| ~ rline(sK8(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(resolution,[],[f921,f961]) ).
fof(f1784,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X0)
| vd684 = vangle(X3,X2,X0)
| ~ ron(X3,sK8(X1,X0))
| ~ ron(X2,sK8(X1,X0))
| X0 = X2
| X2 = X3
| ~ rline(sK8(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f1781]) ).
fof(f1787,plain,
! [X2,X3,X0,X1] :
( ~ ron(X3,sK8(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X0)
| vd684 = vangle(X3,X2,X0)
| X0 = X1
| ~ ron(X2,sK8(X1,X0))
| X0 = X2
| X2 = X3
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f1784,f925]) ).
fof(f1789,plain,
! [X2,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X0,X0)
| vd684 = vangle(X0,X2,X0)
| X0 = X1
| ~ ron(X2,sK8(X1,X0))
| X0 = X2
| X0 = X2
| ~ rpoint(X0)
| ~ rpoint(X2)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f1787,f921]) ).
fof(f1790,plain,
! [X2,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X0,X0)
| vd684 = vangle(X0,X2,X0)
| X0 = X1
| ~ ron(X2,sK8(X1,X0))
| X0 = X2
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f1789]) ).
fof(f1791,plain,
! [X2,X0,X1] :
( ~ ron(X2,sK8(X1,X0))
| ~ rpoint(X1)
| vd684 = vangle(X0,X2,X0)
| X0 = X1
| ~ rpoint(X0)
| X0 = X2
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f1790,f1559]) ).
fof(f1794,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,[],[f923,f1791]) ).
fof(f1798,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,sK8(X1,X0))
| ~ ron(X4,sK8(X1,X0))
| vangle(X5,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X6)
| ~ rline(sK8(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1) ),
inference(resolution,[],[f923,f788]) ).
fof(f1799,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,sK8(X1,X0))
| ~ ron(X4,sK8(X1,X0))
| vangle(X5,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X6)
| ~ rline(sK8(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f1798]) ).
fof(f1803,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X1
| vd684 = vangle(X0,X1,X0) ),
inference(duplicate_literal_removal,[],[f1794]) ).
fof(f1804,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ ron(X5,sK8(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,sK8(X1,X0))
| vangle(X5,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X6)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(forward_subsumption_resolution,[],[f1799,f925]) ).
fof(f1810,plain,
! [X0] :
( ~ rpoint(X0)
| sK1 = X0
| vd684 = vangle(X0,sK1,X0) ),
inference(resolution,[],[f1803,f462]) ).
fof(f1811,plain,
! [X0] :
( ~ rpoint(X0)
| sK2 = X0
| vd684 = vangle(X0,sK2,X0) ),
inference(resolution,[],[f1803,f460]) ).
fof(f1812,plain,
! [X0] :
( ~ rpoint(X0)
| sK3 = X0
| vd684 = vangle(X0,sK3,X0) ),
inference(resolution,[],[f1803,f458]) ).
fof(f1825,plain,
( sK1 = sK2
| vd684 = vangle(sK2,sK1,sK2) ),
inference(resolution,[],[f1810,f460]) ).
fof(f1826,plain,
( sK1 = sK3
| vd684 = vangle(sK3,sK1,sK3) ),
inference(resolution,[],[f1810,f458]) ).
fof(f1827,plain,
vd684 = vangle(sK3,sK1,sK3),
inference(forward_subsumption_resolution,[],[f1826,f757]) ).
fof(f1828,plain,
vd684 = vangle(sK2,sK1,sK2),
inference(forward_subsumption_resolution,[],[f1825,f750]) ).
fof(f1858,plain,
( sF53 = vangle(sK3,sK1,sK1)
| ~ spl54_15 ),
inference(superposition,[],[f1555,f1774]) ).
fof(f1896,plain,
( sK1 = sK3
| vd684 = vangle(sK1,sK3,sK1) ),
inference(resolution,[],[f1812,f462]) ).
fof(f1897,plain,
( sK2 = sK3
| vd684 = vangle(sK2,sK3,sK2) ),
inference(resolution,[],[f1812,f460]) ).
fof(f1899,plain,
vd684 = vangle(sK2,sK3,sK2),
inference(forward_subsumption_resolution,[],[f1897,f761]) ).
fof(f1900,plain,
vd684 = vangle(sK1,sK3,sK1),
inference(forward_subsumption_resolution,[],[f1896,f757]) ).
fof(f1907,definition,
( spl54_23
<=> vd1303 = sK3 ),
introduced(definition,[new_symbols(definition,[spl54_23])],[avatar_definition]) ).
fof(f1908,plain,
( vd1303 != sK3
| spl54_23 ),
inference(avatar_component_clause,[],[f1907]) ).
fof(f1909,plain,
( vd1303 = sK3
| ~ spl54_23 ),
inference(avatar_component_clause,[],[f1907]) ).
fof(f1928,plain,
( sK2 = sK3
| vd684 = vangle(sK3,sK2,sK3) ),
inference(resolution,[],[f1811,f458]) ).
fof(f1929,plain,
vd684 = vangle(sK3,sK2,sK3),
inference(forward_subsumption_resolution,[],[f1928,f761]) ).
fof(f1950,plain,
( vangle(sK3,vd1300,sK1) = vangle(sK3,sK2,sK2)
| ~ spl54_13 ),
inference(superposition,[],[f740,f1749]) ).
fof(f1958,plain,
( sF52 = vangle(sK3,sK2,sK2)
| ~ spl54_13 ),
inference(superposition,[],[f1553,f1749]) ).
fof(f1965,plain,
( vangle(sK3,vd1300,sK1) = sF52
| ~ spl54_13 ),
inference(forward_demodulation,[],[f1950,f1958]) ).
fof(f1969,plain,
( sF52 = vangle(sK3,sK1,sK1)
| ~ spl54_13
| ~ spl54_15 ),
inference(forward_demodulation,[],[f1965,f1774]) ).
fof(f1970,plain,
( sF52 = sF53
| ~ spl54_13
| ~ spl54_15 ),
inference(forward_demodulation,[],[f1969,f1858]) ).
fof(f1971,plain,
( $false
| ~ spl54_13
| ~ spl54_15 ),
inference(forward_subsumption_resolution,[],[f1970,f1556]) ).
fof(f1972,plain,
( ~ spl54_13
| ~ spl54_15 ),
inference(avatar_contradiction_clause,[],[f1971]) ).
fof(f1974,plain,
( vd684 != vf(sK2,sK2)
| ~ spl54_13
| spl54_16 ),
inference(forward_demodulation,[],[f1778,f1749]) ).
fof(f1987,plain,
( $false
| ~ spl54_13
| spl54_16 ),
inference(forward_subsumption_resolution,[],[f1974,f1652]) ).
fof(f1988,plain,
( ~ spl54_13
| spl54_16 ),
inference(avatar_contradiction_clause,[],[f1987]) ).
fof(f2074,plain,
vf(vd1300,sK1) = vf(sK1,vd1300),
inference(resolution,[],[f1715,f462]) ).
fof(f2077,plain,
vf(sK2,vd1306) = vf(sK1,vd1300),
inference(forward_demodulation,[],[f2074,f1767]) ).
fof(f2082,plain,
! [X0] :
( sK1 = sK3
| ~ rpoint(X0)
| sK3 = X0
| vangle(X0,sK1,sK3) = vangle(sK3,sK1,X0) ),
inference(resolution,[],[f1632,f462]) ).
fof(f2086,plain,
! [X0] :
( ~ rpoint(X0)
| sK3 = X0
| vangle(X0,sK1,sK3) = vangle(sK3,sK1,X0) ),
inference(forward_subsumption_resolution,[],[f2082,f757]) ).
fof(f2098,plain,
( rR(sK1,sK3,sK3)
| ~ spl54_23 ),
inference(superposition,[],[f1613,f1909]) ).
fof(f2112,plain,
( ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ spl54_23 ),
inference(resolution,[],[f2098,f1559]) ).
fof(f2119,plain,
( ~ rpoint(sK1)
| ~ spl54_23 ),
inference(forward_subsumption_resolution,[],[f2112,f458]) ).
fof(f2122,plain,
( $false
| ~ spl54_23 ),
inference(forward_subsumption_resolution,[],[f2119,f462]) ).
fof(f2123,plain,
~ spl54_23,
inference(avatar_contradiction_clause,[],[f2122]) ).
fof(f2147,plain,
( sK2 = sK3
| vangle(sK2,sK1,sK3) = vangle(sK3,sK1,sK2) ),
inference(resolution,[],[f2086,f460]) ).
fof(f2149,plain,
vangle(sK2,sK1,sK3) = vangle(sK3,sK1,sK2),
inference(forward_subsumption_resolution,[],[f2147,f761]) ).
fof(f2164,plain,
! [X0] :
( sK2 = sK3
| ~ rpoint(X0)
| sK2 = X0
| vangle(X0,sK3,sK2) = vangle(sK2,sK3,X0) ),
inference(resolution,[],[f1631,f458]) ).
fof(f2165,plain,
! [X0] :
( ~ rpoint(X0)
| sK2 = X0
| vangle(X0,sK3,sK2) = vangle(sK2,sK3,X0) ),
inference(forward_subsumption_resolution,[],[f2164,f761]) ).
fof(f2171,plain,
( vd1306 = sK2
| vangle(sK2,sK3,vd1306) = vangle(vd1306,sK3,sK2) ),
inference(resolution,[],[f2165,f453]) ).
fof(f2174,plain,
( sK1 = sK2
| vangle(sK2,sK3,sK1) = vangle(sK1,sK3,sK2) ),
inference(resolution,[],[f2165,f462]) ).
fof(f2178,plain,
vangle(sK2,sK3,sK1) = vangle(sK1,sK3,sK2),
inference(forward_subsumption_resolution,[],[f2174,f750]) ).
fof(f2181,plain,
( vangle(sK2,sK3,vd1306) = vangle(vd1306,sK3,sK2)
| spl54_13 ),
inference(forward_subsumption_resolution,[],[f2171,f1748]) ).
fof(f2269,plain,
! [X0] :
( ~ rR(sK2,sK3,X0)
| ~ rR(sK2,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1300)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(resolution,[],[f1209,f748]) ).
fof(f2270,plain,
! [X0] :
( ~ rR(sK1,sK3,X0)
| ~ rR(sK1,vd1303,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1303)
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(resolution,[],[f1209,f747]) ).
fof(f2273,plain,
! [X0] :
( ~ rR(sK1,sK3,X0)
| ~ rR(sK1,vd1303,X0)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f2270,f455]) ).
fof(f2274,plain,
! [X0] :
( ~ rR(sK2,sK3,X0)
| ~ rR(sK2,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f2269,f476]) ).
fof(f2279,plain,
! [X0] :
( ~ rR(sK1,sK3,X0)
| ~ rR(sK1,vd1303,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f2273,f462]) ).
fof(f2280,plain,
! [X0] :
( ~ rR(sK2,sK3,X0)
| ~ rR(sK2,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f2274,f460]) ).
fof(f2285,plain,
! [X0] :
( ~ rR(sK1,sK3,X0)
| ~ rR(sK1,vd1303,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2279,f458]) ).
fof(f2286,plain,
! [X0] :
( ~ rR(sK2,sK3,X0)
| ~ rR(sK2,vd1300,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2280,f458]) ).
fof(f2334,plain,
! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ron(sK1,X0)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| sK2 = sK3
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(superposition,[],[f957,f2178]) ).
fof(f2637,plain,
! [X2,X0,X1] :
( vf(sK3,sK1) != vf(sK3,X0)
| X1 = X2
| ~ ron(X0,X2)
| ~ ron(sK2,X1)
| ~ rcenter(sK3,X2)
| ~ rcenter(sK3,X1)
| ~ rpoint(X0)
| ~ rpoint(sK2) ),
inference(superposition,[],[f1507,f749]) ).
fof(f2644,plain,
! [X2,X0,X1] :
( vf(sK3,sK1) != vf(sK3,X0)
| X1 = X2
| ~ ron(X0,X2)
| ~ ron(sK2,X1)
| ~ rcenter(sK3,X2)
| ~ rcenter(sK3,X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2637,f460]) ).
fof(f3886,plain,
! [X0,X1] :
( rinside(X0,sK13(X0,X1))
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f578,f1068]) ).
fof(f3887,plain,
! [X2,X3,X0,X1,X4] :
( X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0)
| X2 = X3
| ~ ron(X2,sK13(X0,X1))
| ~ ron(X3,sK13(X0,X1))
| rR(X0,X3,X2)
| ~ ron(X2,X4)
| ~ ron(X3,X4)
| ~ ron(X0,X4)
| ~ rcircle(sK13(X0,X1))
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X0) ),
inference(resolution,[],[f3886,f1161]) ).
fof(f3888,plain,
! [X2,X3,X0,X1,X4] :
( X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0)
| X2 = X3
| ~ ron(X2,sK13(X0,X1))
| ~ ron(X3,sK13(X0,X1))
| rR(X0,X3,X2)
| ~ ron(X2,X4)
| ~ ron(X3,X4)
| ~ ron(X0,X4)
| ~ rcircle(sK13(X0,X1))
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X3) ),
inference(duplicate_literal_removal,[],[f3887]) ).
fof(f3889,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,sK13(X0,X1))
| ~ rpoint(X1)
| ~ rpoint(X0)
| X2 = X3
| ~ ron(X2,sK13(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,[],[f3888,f1070]) ).
fof(f3957,plain,
! [X0] :
( vd1300 = sK3
| ~ rpoint(X0)
| vd1300 = X0
| vangle(X0,sK3,vd1300) = vangle(vd1300,sK3,X0) ),
inference(resolution,[],[f1629,f458]) ).
fof(f5807,plain,
! [X0,X1] :
( X0 = X1
| ~ ron(sK1,X1)
| ~ ron(sK2,X0)
| ~ rcenter(sK3,X1)
| ~ rcenter(sK3,X0)
| ~ rpoint(sK1) ),
inference(equality_resolution,[],[f2644]) ).
fof(f5814,plain,
! [X0,X1] :
( ~ rcenter(sK3,X1)
| ~ ron(sK1,X1)
| ~ ron(sK2,X0)
| X0 = X1
| ~ rcenter(sK3,X0) ),
inference(forward_subsumption_resolution,[],[f5807,f462]) ).
fof(f5825,plain,
! [X0,X1] :
( ~ ron(sK1,sK13(sK3,X0))
| ~ ron(sK2,X1)
| sK13(sK3,X0) = X1
| ~ rcenter(sK3,X1)
| sK3 = X0
| ~ rpoint(X0)
| ~ rpoint(sK3) ),
inference(resolution,[],[f5814,f1068]) ).
fof(f5826,plain,
! [X0,X1] :
( ~ ron(sK1,sK13(sK3,X0))
| ~ ron(sK2,X1)
| sK13(sK3,X0) = X1
| ~ rcenter(sK3,X1)
| sK3 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f5825,f458]) ).
fof(f5827,plain,
! [X0] :
( ~ ron(sK2,X0)
| sK13(sK3,sK1) = X0
| ~ rcenter(sK3,X0)
| sK1 = sK3
| ~ rpoint(sK1)
| sK1 = sK3
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(resolution,[],[f5826,f1066]) ).
fof(f5828,plain,
! [X0] :
( ~ ron(sK2,X0)
| sK13(sK3,sK1) = X0
| ~ rcenter(sK3,X0)
| sK1 = sK3
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(duplicate_literal_removal,[],[f5827]) ).
fof(f5829,plain,
! [X0] :
( ~ ron(sK2,X0)
| sK13(sK3,sK1) = X0
| ~ rcenter(sK3,X0)
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f5828,f757]) ).
fof(f5830,plain,
! [X0] :
( ~ ron(sK2,X0)
| sK13(sK3,sK1) = X0
| ~ rcenter(sK3,X0)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f5829,f462]) ).
fof(f5831,plain,
! [X0] :
( ~ rcenter(sK3,X0)
| sK13(sK3,sK1) = X0
| ~ ron(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f5830,f458]) ).
fof(f5832,plain,
! [X0] :
( sK13(sK3,X0) = sK13(sK3,sK1)
| ~ ron(sK2,sK13(sK3,X0))
| sK3 = X0
| ~ rpoint(X0)
| ~ rpoint(sK3) ),
inference(resolution,[],[f5831,f1068]) ).
fof(f5833,plain,
! [X0] :
( ~ ron(sK2,sK13(sK3,X0))
| sK13(sK3,X0) = sK13(sK3,sK1)
| sK3 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f5832,f458]) ).
fof(f5834,plain,
( sK13(sK3,sK1) = sK13(sK3,sK2)
| sK2 = sK3
| ~ rpoint(sK2)
| sK2 = sK3
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(resolution,[],[f5833,f1066]) ).
fof(f5835,plain,
( sK13(sK3,sK1) = sK13(sK3,sK2)
| sK2 = sK3
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(duplicate_literal_removal,[],[f5834]) ).
fof(f5836,plain,
( sK13(sK3,sK1) = sK13(sK3,sK2)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f5835,f761]) ).
fof(f5837,plain,
( sK13(sK3,sK1) = sK13(sK3,sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f5836,f460]) ).
fof(f5838,plain,
sK13(sK3,sK1) = sK13(sK3,sK2),
inference(forward_subsumption_resolution,[],[f5837,f458]) ).
fof(f5843,plain,
( ron(sK2,sK13(sK3,sK1))
| sK2 = sK3
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(superposition,[],[f1066,f5838]) ).
fof(f5844,plain,
( ron(sK2,sK13(sK3,sK1))
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f5843,f761]) ).
fof(f5848,plain,
( ron(sK2,sK13(sK3,sK1))
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f5844,f460]) ).
fof(f5852,plain,
ron(sK2,sK13(sK3,sK1)),
inference(forward_subsumption_resolution,[],[f5848,f458]) ).
fof(f7878,plain,
( vangle(sK2,sK3,sK1) = vangle(vd1306,sK3,sK2)
| spl54_13 ),
inference(forward_demodulation,[],[f2181,f743]) ).
fof(f7966,plain,
! [X0] :
( ~ rpoint(X0)
| vd1300 = X0
| vangle(X0,sK3,vd1300) = vangle(vd1300,sK3,X0) ),
inference(forward_subsumption_resolution,[],[f3957,f758]) ).
fof(f8037,plain,
( vangle(vd1306,sK3,sK2) = vangle(sK1,sK3,sK2)
| spl54_13 ),
inference(forward_demodulation,[],[f7878,f2178]) ).
fof(f8300,plain,
( ! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ron(sK2,X0)
| ~ ron(vd1306,X0)
| ~ ron(sK3,X0)
| sK2 = sK3
| vd1306 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(vd1306)
| ~ rpoint(sK3) )
| spl54_13 ),
inference(superposition,[],[f957,f8037]) ).
fof(f8891,plain,
( vd1300 = sK1
| vangle(vd1300,sK3,sK1) = vangle(sK1,sK3,vd1300) ),
inference(resolution,[],[f7966,f462]) ).
fof(f9092,plain,
( vd684 != vf(sK1,vd1300)
| vd1306 = sK2
| ~ rpoint(vd1306)
| ~ rpoint(sK2) ),
inference(superposition,[],[f977,f2077]) ).
fof(f9104,plain,
( vd684 != vf(sK1,vd1300)
| ~ rpoint(vd1306)
| ~ rpoint(sK2)
| spl54_13 ),
inference(forward_subsumption_resolution,[],[f9092,f1748]) ).
fof(f21270,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK2,X0,X1)
| rR(sK2,X2,X3)
| sK2 = X1
| sK2 = X3
| sK2 = X0
| sK2 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1295)
| ~ ron(X2,vd1295)
| vangle(X3,sK2,X1) = vangle(X2,sK2,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f1620,f505]) ).
fof(f21271,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK3,X0,X1)
| rR(sK3,X2,X3)
| sK3 = X1
| sK3 = X3
| sK3 = X0
| sK3 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1295)
| ~ ron(X2,vd1295)
| vangle(X3,sK3,X1) = vangle(X2,sK3,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1619,f505]) ).
fof(f21272,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK3,X0,X1)
| rR(sK3,X2,X3)
| sK3 = X1
| sK3 = X3
| sK3 = X0
| sK3 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK3,X1) = vangle(X2,sK3,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1623,f502]) ).
fof(f21274,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK1,X0,X1)
| rR(sK1,X2,X3)
| sK1 = X1
| sK1 = X3
| sK1 = X0
| sK1 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK1,X1) = vangle(X2,sK1,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f1625,f502]) ).
fof(f21280,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,[],[f1647,f502]) ).
fof(f21287,plain,
! [X0,X1] :
( rR(X0,X1,vd1303)
| vd684 = vangle(X1,X0,vd1303)
| ~ ron(X1,vd1297)
| ~ ron(X0,vd1297)
| vd1303 = X0
| X0 = X1
| ~ rpoint(vd1303)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1654,f502]) ).
fof(f21294,plain,
! [X0,X1] :
( ~ ron(X0,X1)
| ~ ron(X0,vd1295)
| ~ ron(sK3,X1)
| vd1295 = X1
| ~ rline(X1)
| sK3 = X0
| ~ rpoint(X0)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1677,f505]) ).
fof(f21330,plain,
! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ron(sK1,X0)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| sK2 = sK3
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f2334,f757]) ).
fof(f21498,plain,
( ! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ron(sK2,X0)
| ~ ron(vd1306,X0)
| ~ ron(sK3,X0)
| vd1306 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(vd1306)
| ~ rpoint(sK3) )
| spl54_13 ),
inference(forward_subsumption_resolution,[],[f8300,f761]) ).
fof(f21846,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,vd1295)
| rR(sK2,X2,X3)
| sK2 = X1
| sK2 = X3
| sK2 = X0
| sK2 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| rR(sK2,X0,X1)
| ~ ron(X2,vd1295)
| vangle(X3,sK2,X1) = vangle(X2,sK2,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f21270,f460]) ).
fof(f21847,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,vd1295)
| rR(sK3,X2,X3)
| sK3 = X1
| sK3 = X3
| sK3 = X0
| sK3 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| rR(sK3,X0,X1)
| ~ ron(X2,vd1295)
| vangle(X3,sK3,X1) = vangle(X2,sK3,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f21271,f458]) ).
fof(f21848,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,vd1297)
| rR(sK3,X2,X3)
| sK3 = X1
| sK3 = X3
| sK3 = X0
| sK3 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| rR(sK3,X0,X1)
| ~ ron(X2,vd1297)
| vangle(X3,sK3,X1) = vangle(X2,sK3,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f21272,f458]) ).
fof(f21850,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,vd1297)
| rR(sK1,X2,X3)
| sK1 = X1
| sK1 = X3
| sK1 = X0
| sK1 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| rR(sK1,X0,X1)
| ~ ron(X2,vd1297)
| vangle(X3,sK1,X1) = vangle(X2,sK1,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f21274,f462]) ).
fof(f21856,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,[],[f21280,f453]) ).
fof(f21863,plain,
! [X0,X1] :
( rR(X0,X1,vd1303)
| vd684 = vangle(X1,X0,vd1303)
| ~ ron(X1,vd1297)
| ~ ron(X0,vd1297)
| vd1303 = X0
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f21287,f455]) ).
fof(f21870,plain,
! [X0,X1] :
( ~ ron(sK3,X1)
| ~ ron(X0,vd1295)
| ~ ron(X0,X1)
| vd1295 = X1
| ~ rline(X1)
| sK3 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f21294,f458]) ).
fof(f21904,plain,
! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ron(sK1,X0)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f21330,f761]) ).
fof(f22086,plain,
( ! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ron(sK2,X0)
| ~ ron(vd1306,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(vd1306)
| ~ rpoint(sK3) )
| spl54_13 ),
inference(forward_subsumption_resolution,[],[f21498,f755]) ).
fof(f22958,plain,
! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ron(sK1,X0)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f21904,f462]) ).
fof(f23312,plain,
( ! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ron(sK2,X0)
| ~ ron(vd1306,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(vd1306)
| ~ rpoint(sK3) )
| spl54_13 ),
inference(forward_subsumption_resolution,[],[f22086,f460]) ).
fof(f23575,plain,
! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ron(sK1,X0)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f22958,f460]) ).
fof(f23718,plain,
( ! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ron(sK2,X0)
| ~ ron(vd1306,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK3) )
| spl54_13 ),
inference(forward_subsumption_resolution,[],[f23312,f453]) ).
fof(f23964,plain,
! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ron(sK1,X0)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f23575,f458]) ).
fof(f24026,plain,
( ! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ron(sK2,X0)
| ~ ron(vd1306,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) )
| spl54_13 ),
inference(forward_subsumption_resolution,[],[f23718,f458]) ).
fof(f24187,definition,
( spl54_1293
<=> ! [X0] :
( ~ ron(sK3,X0)
| ~ rline(X0)
| ~ ron(sK1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_1293])],[avatar_definition]) ).
fof(f24188,plain,
( ! [X0] :
( ~ ron(sK3,X0)
| ~ rline(X0)
| ~ ron(sK1,X0) )
| ~ spl54_1293 ),
inference(avatar_component_clause,[],[f24187]) ).
fof(f24190,definition,
( spl54_1294
<=> rR(sK1,sK3,vd1300) ),
introduced(definition,[new_symbols(definition,[spl54_1294])],[avatar_definition]) ).
fof(f24191,plain,
( rR(sK1,sK3,vd1300)
| ~ spl54_1294 ),
inference(avatar_component_clause,[],[f24190]) ).
fof(f24192,plain,
( ~ rR(sK1,sK3,vd1300)
| spl54_1294 ),
inference(avatar_component_clause,[],[f24190]) ).
fof(f24194,definition,
( spl54_1295
<=> vd684 = sF53 ),
introduced(definition,[new_symbols(definition,[spl54_1295])],[avatar_definition]) ).
fof(f24195,plain,
( vd684 = sF53
| ~ spl54_1295 ),
inference(avatar_component_clause,[],[f24194]) ).
fof(f24196,plain,
( vd684 != sF53
| spl54_1295 ),
inference(avatar_component_clause,[],[f24194]) ).
fof(f24222,definition,
( spl54_1300
<=> vd684 = vangle(sK1,sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl54_1300])],[avatar_definition]) ).
fof(f24223,plain,
( vd684 = vangle(sK1,sK3,sK2)
| ~ spl54_1300 ),
inference(avatar_component_clause,[],[f24222]) ).
fof(f24224,plain,
( vd684 != vangle(sK1,sK3,sK2)
| spl54_1300 ),
inference(avatar_component_clause,[],[f24222]) ).
fof(f24236,definition,
( spl54_1303
<=> vd684 = vangle(sK3,sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl54_1303])],[avatar_definition]) ).
fof(f24237,plain,
( vd684 = vangle(sK3,sK1,sK2)
| ~ spl54_1303 ),
inference(avatar_component_clause,[],[f24236]) ).
fof(f24238,plain,
( vd684 != vangle(sK3,sK1,sK2)
| spl54_1303 ),
inference(avatar_component_clause,[],[f24236]) ).
fof(f24245,definition,
( spl54_1305
<=> ! [X0] :
( ~ ron(sK2,X0)
| ~ rline(X0)
| ~ ron(sK3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_1305])],[avatar_definition]) ).
fof(f24246,plain,
( ! [X0] :
( ~ ron(sK2,X0)
| ~ rline(X0)
| ~ ron(sK3,X0) )
| ~ spl54_1305 ),
inference(avatar_component_clause,[],[f24245]) ).
fof(f24253,definition,
( spl54_1307
<=> ! [X0] :
( ron(sK1,X0)
| ~ rline(X0)
| ~ ron(sK3,X0)
| ~ ron(sK2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_1307])],[avatar_definition]) ).
fof(f24254,plain,
( ! [X0] :
( ~ ron(sK3,X0)
| ~ rline(X0)
| ron(sK1,X0)
| ~ ron(sK2,X0) )
| ~ spl54_1307 ),
inference(avatar_component_clause,[],[f24253]) ).
fof(f24255,plain,
( spl54_1307
| ~ spl54_1300 ),
inference(avatar_split_clause,[],[f23964,f24222,f24253]) ).
fof(f24320,definition,
( spl54_1319
<=> rR(sK3,sK1,vd1300) ),
introduced(definition,[new_symbols(definition,[spl54_1319])],[avatar_definition]) ).
fof(f24322,plain,
( ~ rR(sK3,sK1,vd1300)
| spl54_1319 ),
inference(avatar_component_clause,[],[f24320]) ).
fof(f24384,definition,
( spl54_1320
<=> vd684 = sF52 ),
introduced(definition,[new_symbols(definition,[spl54_1320])],[avatar_definition]) ).
fof(f24385,plain,
( vd684 = sF52
| ~ spl54_1320 ),
inference(avatar_component_clause,[],[f24384]) ).
fof(f24386,plain,
( vd684 != sF52
| spl54_1320 ),
inference(avatar_component_clause,[],[f24384]) ).
fof(f24529,definition,
( spl54_1333
<=> ! [X0] :
( ~ ron(sK1,X0)
| ~ rline(X0)
| ~ ron(sK3,X0)
| ron(sK2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_1333])],[avatar_definition]) ).
fof(f24530,plain,
( ! [X0] :
( ~ ron(sK3,X0)
| ~ rline(X0)
| ~ ron(sK1,X0)
| ron(sK2,X0) )
| ~ spl54_1333 ),
inference(avatar_component_clause,[],[f24529]) ).
fof(f24685,definition,
( spl54_1346
<=> rR(sK3,sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl54_1346])],[avatar_definition]) ).
fof(f24686,plain,
( rR(sK3,sK1,sK2)
| ~ spl54_1346 ),
inference(avatar_component_clause,[],[f24685]) ).
fof(f24687,plain,
( ~ rR(sK3,sK1,sK2)
| spl54_1346 ),
inference(avatar_component_clause,[],[f24685]) ).
fof(f26672,plain,
! [X2,X3,X0,X1] :
( rR(sK2,X0,sK3)
| sK2 = X1
| sK2 = sK3
| sK2 = X2
| sK2 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK2,X2,X1)
| ~ ron(X0,vd1295)
| vangle(sK3,sK2,X1) = vangle(X0,sK2,X2)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK3)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f21846,f772]) ).
fof(f26693,plain,
! [X2,X3,X0,X1] :
( rR(sK2,X0,sK3)
| sK2 = X1
| sK2 = X2
| sK2 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK2,X2,X1)
| ~ ron(X0,vd1295)
| vangle(sK3,sK2,X1) = vangle(X0,sK2,X2)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK3)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26672,f761]) ).
fof(f26701,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,X3)
| sK2 = X1
| sK2 = X2
| sK2 = X0
| ~ ron(X1,X3)
| rR(sK2,X0,sK3)
| rR(sK2,X2,X1)
| ~ ron(X0,vd1295)
| vangle(sK3,sK2,X1) = vangle(X0,sK2,X2)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26693,f458]) ).
fof(f26750,plain,
! [X0,X1] :
( sK2 = X0
| sK2 = sK3
| sK2 = X1
| ~ ron(X0,vd1297)
| rR(sK2,X1,sK3)
| rR(sK2,sK3,X0)
| ~ ron(X1,vd1295)
| vangle(sK3,sK2,X0) = vangle(X1,sK2,sK3)
| ~ rline(vd1297)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(X1) ),
inference(resolution,[],[f26701,f770]) ).
fof(f26798,plain,
! [X0,X1] :
( sK2 = X0
| sK2 = X1
| ~ ron(X0,vd1297)
| rR(sK2,X1,sK3)
| rR(sK2,sK3,X0)
| ~ ron(X1,vd1295)
| vangle(sK3,sK2,X0) = vangle(X1,sK2,sK3)
| ~ rline(vd1297)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26750,f761]) ).
fof(f26810,plain,
! [X0,X1] :
( sK2 = X0
| sK2 = X1
| ~ ron(X0,vd1297)
| rR(sK2,X1,sK3)
| rR(sK2,sK3,X0)
| ~ ron(X1,vd1295)
| vangle(sK3,sK2,X0) = vangle(X1,sK2,sK3)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26798,f502]) ).
fof(f26822,plain,
! [X0,X1] :
( rR(sK2,sK3,X0)
| rR(sK2,X1,sK3)
| ~ ron(X0,vd1297)
| sK2 = X1
| sK2 = X0
| ~ ron(X1,vd1295)
| vangle(sK3,sK2,X0) = vangle(X1,sK2,sK3)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26810,f458]) ).
fof(f26838,plain,
! [X2,X3,X0,X1] :
( rR(sK3,X0,sK2)
| sK3 = X1
| sK2 = sK3
| sK3 = X2
| sK3 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK3,X2,X1)
| ~ ron(X0,vd1295)
| vangle(X0,sK3,X2) = vangle(sK2,sK3,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK2)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f21847,f769]) ).
fof(f26852,plain,
! [X2,X3,X0,X1] :
( rR(sK3,X0,sK2)
| sK3 = X1
| sK3 = X2
| sK3 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK3,X2,X1)
| ~ ron(X0,vd1295)
| vangle(X0,sK3,X2) = vangle(sK2,sK3,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK2)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26838,f761]) ).
fof(f26854,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,X3)
| sK3 = X1
| sK3 = X2
| sK3 = X0
| ~ ron(X1,X3)
| rR(sK3,X0,sK2)
| rR(sK3,X2,X1)
| ~ ron(X0,vd1295)
| vangle(X0,sK3,X2) = vangle(sK2,sK3,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26852,f460]) ).
fof(f26882,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,sK8(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,[],[f1804,f921]) ).
fof(f26896,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ ron(X4,sK8(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,[],[f26882]) ).
fof(f26922,plain,
! [X0,X1] :
( sK3 = X0
| sK1 = sK3
| sK3 = X1
| ~ ron(X0,vd1297)
| rR(sK3,X1,sK2)
| rR(sK3,sK1,X0)
| ~ ron(X1,vd1295)
| vangle(sK2,sK3,X0) = vangle(X1,sK3,sK1)
| ~ rline(vd1297)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(X1) ),
inference(resolution,[],[f26854,f768]) ).
fof(f26973,plain,
! [X0,X1] :
( sK3 = X0
| sK3 = X1
| ~ ron(X0,vd1297)
| rR(sK3,X1,sK2)
| rR(sK3,sK1,X0)
| ~ ron(X1,vd1295)
| vangle(sK2,sK3,X0) = vangle(X1,sK3,sK1)
| ~ rline(vd1297)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26922,f757]) ).
fof(f26985,plain,
! [X0,X1] :
( sK3 = X0
| sK3 = X1
| ~ ron(X0,vd1297)
| rR(sK3,X1,sK2)
| rR(sK3,sK1,X0)
| ~ ron(X1,vd1295)
| vangle(sK2,sK3,X0) = vangle(X1,sK3,sK1)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26973,f502]) ).
fof(f26997,plain,
! [X0,X1] :
( rR(sK3,sK1,X0)
| rR(sK3,X1,sK2)
| ~ ron(X0,vd1297)
| sK3 = X1
| sK3 = X0
| ~ ron(X1,vd1295)
| vangle(sK2,sK3,X0) = vangle(X1,sK3,sK1)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26985,f462]) ).
fof(f27011,plain,
! [X2,X3,X0,X1] :
( rR(sK3,X0,sK1)
| sK3 = X1
| sK1 = sK3
| sK3 = X2
| sK3 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK3,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK3,X2) = vangle(sK1,sK3,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f21848,f768]) ).
fof(f27029,plain,
! [X2,X3,X0,X1] :
( rR(sK3,X0,sK1)
| sK3 = X1
| sK3 = X2
| sK3 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK3,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK3,X2) = vangle(sK1,sK3,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f27011,f757]) ).
fof(f27037,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,X3)
| sK3 = X1
| sK3 = X2
| sK3 = X0
| ~ ron(X1,X3)
| rR(sK3,X0,sK1)
| rR(sK3,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK3,X2) = vangle(sK1,sK3,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f27029,f462]) ).
fof(f27046,definition,
( spl54_1554
<=> ron(sK2,vd1297) ),
introduced(definition,[new_symbols(definition,[spl54_1554])],[avatar_definition]) ).
fof(f27047,plain,
( ron(sK2,vd1297)
| ~ spl54_1554 ),
inference(avatar_component_clause,[],[f27046]) ).
fof(f27048,plain,
( ~ ron(sK2,vd1297)
| spl54_1554 ),
inference(avatar_component_clause,[],[f27046]) ).
fof(f27069,plain,
! [X2,X3,X0,X1] :
( rR(sK1,X0,sK3)
| sK1 = X1
| sK1 = sK3
| sK1 = X2
| sK1 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK1,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK1,X2) = vangle(sK3,sK1,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK3)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f21850,f770]) ).
fof(f27081,plain,
! [X2,X3,X0,X1] :
( rR(sK1,X0,sK3)
| sK1 = X1
| sK1 = X2
| sK1 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK1,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK1,X2) = vangle(sK3,sK1,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK3)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f27069,f757]) ).
fof(f27084,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,X3)
| sK1 = X1
| sK1 = X2
| sK1 = X0
| ~ ron(X1,X3)
| rR(sK1,X0,sK3)
| rR(sK1,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK1,X2) = vangle(sK3,sK1,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f27081,f458]) ).
fof(f27102,plain,
! [X0,X1] :
( sK1 = X0
| sK1 = sK3
| sK1 = X1
| ~ ron(X0,vd1295)
| rR(sK1,X1,sK3)
| rR(sK1,sK3,X0)
| ~ ron(X1,vd1297)
| vangle(sK3,sK1,X0) = vangle(X1,sK1,sK3)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(X1) ),
inference(resolution,[],[f27084,f772]) ).
fof(f27151,plain,
! [X0,X1] :
( sK1 = X0
| sK1 = X1
| ~ ron(X0,vd1295)
| rR(sK1,X1,sK3)
| rR(sK1,sK3,X0)
| ~ ron(X1,vd1297)
| vangle(sK3,sK1,X0) = vangle(X1,sK1,sK3)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f27102,f757]) ).
fof(f27165,plain,
! [X0,X1] :
( sK1 = X0
| sK1 = X1
| ~ ron(X0,vd1295)
| rR(sK1,X1,sK3)
| rR(sK1,sK3,X0)
| ~ ron(X1,vd1297)
| vangle(sK3,sK1,X0) = vangle(X1,sK1,sK3)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f27151,f505]) ).
fof(f27179,plain,
! [X0,X1] :
( rR(sK1,sK3,X0)
| rR(sK1,X1,sK3)
| ~ ron(X0,vd1295)
| sK1 = X1
| sK1 = X0
| ~ ron(X1,vd1297)
| vangle(sK3,sK1,X0) = vangle(X1,sK1,sK3)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f27165,f458]) ).
fof(f27312,definition,
( spl54_1564
<=> rR(sK1,vd1303,sK2) ),
introduced(definition,[new_symbols(definition,[spl54_1564])],[avatar_definition]) ).
fof(f27313,plain,
( ~ rR(sK1,vd1303,sK2)
| spl54_1564 ),
inference(avatar_component_clause,[],[f27312]) ).
fof(f27410,definition,
( spl54_1566
<=> ron(vd1300,vd1297) ),
introduced(definition,[new_symbols(definition,[spl54_1566])],[avatar_definition]) ).
fof(f27411,plain,
( ron(vd1300,vd1297)
| ~ spl54_1566 ),
inference(avatar_component_clause,[],[f27410]) ).
fof(f27412,plain,
( ~ ron(vd1300,vd1297)
| spl54_1566 ),
inference(avatar_component_clause,[],[f27410]) ).
fof(f27435,definition,
( spl54_1569
<=> vd684 = vangle(sK1,sK3,vd1306) ),
introduced(definition,[new_symbols(definition,[spl54_1569])],[avatar_definition]) ).
fof(f27436,plain,
( vd684 != vangle(sK1,sK3,vd1306)
| spl54_1569 ),
inference(avatar_component_clause,[],[f27435]) ).
fof(f27437,plain,
( vd684 = vangle(sK1,sK3,vd1306)
| ~ spl54_1569 ),
inference(avatar_component_clause,[],[f27435]) ).
fof(f27605,plain,
! [X0,X1] :
( sK3 = X0
| sK1 = sK3
| sK3 = X1
| ~ ron(X0,vd1297)
| rR(sK3,X1,sK1)
| rR(sK3,sK1,X0)
| ~ ron(X1,vd1297)
| vangle(sK1,sK3,X0) = vangle(X1,sK3,sK1)
| ~ rline(vd1297)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(X1) ),
inference(resolution,[],[f27037,f768]) ).
fof(f27656,plain,
! [X0,X1] :
( sK3 = X0
| sK3 = X1
| ~ ron(X0,vd1297)
| rR(sK3,X1,sK1)
| rR(sK3,sK1,X0)
| ~ ron(X1,vd1297)
| vangle(sK1,sK3,X0) = vangle(X1,sK3,sK1)
| ~ rline(vd1297)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f27605,f757]) ).
fof(f27668,plain,
! [X0,X1] :
( sK3 = X0
| sK3 = X1
| ~ ron(X0,vd1297)
| rR(sK3,X1,sK1)
| rR(sK3,sK1,X0)
| ~ ron(X1,vd1297)
| vangle(sK1,sK3,X0) = vangle(X1,sK3,sK1)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f27656,f502]) ).
fof(f27680,plain,
! [X0,X1] :
( rR(sK3,sK1,X0)
| rR(sK3,X1,sK1)
| ~ ron(X0,vd1297)
| sK3 = X1
| sK3 = X0
| ~ ron(X1,vd1297)
| vangle(sK1,sK3,X0) = vangle(X1,sK3,sK1)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f27668,f462]) ).
fof(f27717,plain,
! [X0] :
( rR(sK2,sK3,X0)
| ~ ron(X0,vd1297)
| sK2 = sK3
| sK2 = X0
| ~ ron(sK3,vd1295)
| vangle(sK3,sK2,sK3) = vangle(sK3,sK2,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK3)
| ~ rpoint(sK2) ),
inference(resolution,[],[f26822,f1559]) ).
fof(f27720,plain,
! [X0] :
( rR(sK2,sK3,X0)
| ~ ron(X0,vd1297)
| sK2 = sK3
| sK2 = X0
| ~ ron(sK3,vd1295)
| vangle(sK3,sK2,sK3) = vangle(sK3,sK2,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK2) ),
inference(duplicate_literal_removal,[],[f27717]) ).
fof(f27744,plain,
! [X0] :
( rR(sK2,sK3,X0)
| ~ ron(X0,vd1297)
| sK2 = X0
| ~ ron(sK3,vd1295)
| vangle(sK3,sK2,sK3) = vangle(sK3,sK2,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f27720,f761]) ).
fof(f27764,plain,
! [X0] :
( rR(sK2,sK3,X0)
| ~ ron(X0,vd1297)
| sK2 = X0
| vangle(sK3,sK2,sK3) = vangle(sK3,sK2,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f27744,f772]) ).
fof(f27784,plain,
! [X0] :
( rR(sK2,sK3,X0)
| ~ ron(X0,vd1297)
| sK2 = X0
| vangle(sK3,sK2,sK3) = vangle(sK3,sK2,X0)
| ~ rpoint(X0)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f27764,f458]) ).
fof(f27792,plain,
! [X0] :
( rR(sK2,sK3,X0)
| ~ ron(X0,vd1297)
| sK2 = X0
| vangle(sK3,sK2,sK3) = vangle(sK3,sK2,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f27784,f460]) ).
fof(f27798,plain,
! [X0] :
( rR(sK2,sK3,X0)
| vd684 = vangle(sK3,sK2,X0)
| ~ ron(X0,vd1297)
| sK2 = X0
| ~ rpoint(X0) ),
inference(forward_demodulation,[],[f27792,f1929]) ).
fof(f27802,definition,
( spl54_1572
<=> rR(sK2,sK3,vd1303) ),
introduced(definition,[new_symbols(definition,[spl54_1572])],[avatar_definition]) ).
fof(f27804,plain,
( rR(sK2,sK3,vd1303)
| ~ spl54_1572 ),
inference(avatar_component_clause,[],[f27802]) ).
fof(f27854,plain,
( vd684 = vangle(sK3,sK2,vd1306)
| ~ ron(vd1306,vd1297)
| vd1306 = sK2
| ~ rpoint(vd1306)
| rR(sK2,sK3,vd1303)
| ~ rpoint(sK2) ),
inference(resolution,[],[f27798,f1710]) ).
fof(f27888,plain,
( vd684 = vangle(sK3,sK2,vd1306)
| vd1306 = sK2
| ~ rpoint(vd1306)
| rR(sK2,sK3,vd1303)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f27854,f515]) ).
fof(f27898,plain,
( vd684 = vangle(sK3,sK2,vd1306)
| ~ rpoint(vd1306)
| rR(sK2,sK3,vd1303)
| ~ rpoint(sK2)
| spl54_13 ),
inference(forward_subsumption_resolution,[],[f27888,f1748]) ).
fof(f27902,plain,
( vd684 = vangle(sK3,sK2,vd1306)
| rR(sK2,sK3,vd1303)
| ~ rpoint(sK2)
| spl54_13 ),
inference(forward_subsumption_resolution,[],[f27898,f453]) ).
fof(f27905,plain,
( vd684 = vangle(sK3,sK2,vd1306)
| rR(sK2,sK3,vd1303)
| spl54_13 ),
inference(forward_subsumption_resolution,[],[f27902,f460]) ).
fof(f27907,plain,
( vd684 = sF52
| rR(sK2,sK3,vd1303)
| spl54_13 ),
inference(forward_demodulation,[],[f27905,f1553]) ).
fof(f27909,plain,
( rR(sK2,sK3,vd1303)
| spl54_13
| spl54_1320 ),
inference(forward_subsumption_resolution,[],[f27907,f24386]) ).
fof(f27910,plain,
( spl54_1572
| spl54_13
| spl54_1320 ),
inference(avatar_split_clause,[],[f27909,f24384,f1747,f27802]) ).
fof(f27911,plain,
( ~ rR(sK2,vd1300,vd1303)
| ~ rpoint(vd1303)
| ~ spl54_1572 ),
inference(resolution,[],[f27804,f2286]) ).
fof(f27928,plain,
( ~ rR(sK2,vd1300,vd1303)
| ~ spl54_1572 ),
inference(forward_subsumption_resolution,[],[f27911,f455]) ).
fof(f28423,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,[],[f26896,f921]) ).
fof(f28437,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,[],[f28423]) ).
fof(f28444,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,[],[f28437,f1559]) ).
fof(f28467,plain,
! [X2,X0,X1] :
( rR(X0,X1,sK2)
| sK2 = X0
| X0 = X2
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,vd1295)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,sK2)
| ~ rline(vd1295)
| ~ rpoint(sK2)
| ~ rpoint(X1) ),
inference(resolution,[],[f28444,f769]) ).
fof(f28497,plain,
! [X2,X3,X0,X1,X4] :
( rR(X0,X1,X2)
| X0 = X2
| X0 = X3
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,sK8(X4,X2))
| ~ rpoint(X3)
| vangle(X3,X0,X2) = vangle(X3,X0,X1)
| ~ rline(sK8(X4,X2))
| ~ rpoint(X2)
| ~ rpoint(X1)
| X2 = X4
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(resolution,[],[f28444,f921]) ).
fof(f28508,plain,
! [X2,X3,X0,X1,X4] :
( rR(X0,X1,X2)
| X0 = X2
| X0 = X3
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,sK8(X4,X2))
| ~ rpoint(X3)
| vangle(X3,X0,X2) = vangle(X3,X0,X1)
| ~ rline(sK8(X4,X2))
| ~ rpoint(X2)
| ~ rpoint(X1)
| X2 = X4
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f28497]) ).
fof(f28512,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X1,sK8(X4,X2))
| X0 = X2
| X0 = X3
| X0 = X1
| ~ rpoint(X0)
| rR(X0,X1,X2)
| ~ rpoint(X3)
| vangle(X3,X0,X2) = vangle(X3,X0,X1)
| ~ rpoint(X2)
| ~ rpoint(X1)
| X2 = X4
| ~ rpoint(X4) ),
inference(forward_subsumption_resolution,[],[f28508,f925]) ).
fof(f28514,plain,
! [X2,X0,X1] :
( rR(X0,X1,sK2)
| sK2 = X0
| X0 = X2
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,vd1295)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,sK2)
| ~ rpoint(sK2)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f28467,f505]) ).
fof(f28529,plain,
! [X2,X0,X1] :
( ~ ron(X1,vd1295)
| sK2 = X0
| X0 = X2
| X0 = X1
| ~ rpoint(X0)
| rR(X0,X1,sK2)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,sK2)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f28514,f460]) ).
fof(f28574,plain,
! [X0] :
( rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK2 = sK3
| sK3 = X0
| ~ ron(sK2,vd1295)
| vangle(sK2,sK3,sK1) = vangle(sK2,sK3,X0)
| ~ rpoint(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(resolution,[],[f26997,f1559]) ).
fof(f28577,plain,
! [X0] :
( rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK2 = sK3
| sK3 = X0
| ~ ron(sK2,vd1295)
| vangle(sK2,sK3,sK1) = vangle(sK2,sK3,X0)
| ~ rpoint(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(duplicate_literal_removal,[],[f28574]) ).
fof(f28600,plain,
! [X0] :
( rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK3 = X0
| ~ ron(sK2,vd1295)
| vangle(sK2,sK3,sK1) = vangle(sK2,sK3,X0)
| ~ rpoint(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f28577,f761]) ).
fof(f28621,plain,
! [X0] :
( rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK3 = X0
| vangle(sK2,sK3,sK1) = vangle(sK2,sK3,X0)
| ~ rpoint(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f28600,f769]) ).
fof(f28642,plain,
! [X0] :
( rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK3 = X0
| vangle(sK2,sK3,sK1) = vangle(sK2,sK3,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f28621,f460]) ).
fof(f28651,plain,
! [X0] :
( rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK3 = X0
| vangle(sK2,sK3,sK1) = vangle(sK2,sK3,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f28642,f458]) ).
fof(f28657,plain,
! [X0] :
( vangle(sK2,sK3,X0) = vangle(sK1,sK3,sK2)
| rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK3 = X0
| ~ rpoint(X0) ),
inference(forward_demodulation,[],[f28651,f2178]) ).
fof(f28659,definition,
( spl54_1579
<=> ! [X0] :
( vangle(sK2,sK3,X0) = vangle(sK1,sK3,sK2)
| ~ rpoint(X0)
| sK3 = X0
| ~ ron(X0,vd1297)
| rR(sK3,sK1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_1579])],[avatar_definition]) ).
fof(f28660,plain,
( ! [X0] :
( rR(sK3,sK1,X0)
| ~ rpoint(X0)
| sK3 = X0
| ~ ron(X0,vd1297)
| vangle(sK2,sK3,X0) = vangle(sK1,sK3,sK2) )
| ~ spl54_1579 ),
inference(avatar_component_clause,[],[f28659]) ).
fof(f28665,plain,
spl54_1579,
inference(avatar_split_clause,[],[f28657,f28659]) ).
fof(f29116,plain,
! [X0] :
( rR(sK1,sK3,X0)
| ~ ron(X0,vd1295)
| sK1 = sK3
| sK1 = X0
| ~ ron(sK3,vd1297)
| vangle(sK3,sK1,sK3) = vangle(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(resolution,[],[f27179,f1559]) ).
fof(f29119,plain,
! [X0] :
( rR(sK1,sK3,X0)
| ~ ron(X0,vd1295)
| sK1 = sK3
| sK1 = X0
| ~ ron(sK3,vd1297)
| vangle(sK3,sK1,sK3) = vangle(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(duplicate_literal_removal,[],[f29116]) ).
fof(f29143,plain,
! [X0] :
( rR(sK1,sK3,X0)
| ~ ron(X0,vd1295)
| sK1 = X0
| ~ ron(sK3,vd1297)
| vangle(sK3,sK1,sK3) = vangle(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f29119,f757]) ).
fof(f29162,plain,
! [X0] :
( rR(sK1,sK3,X0)
| ~ ron(X0,vd1295)
| sK1 = X0
| vangle(sK3,sK1,sK3) = vangle(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f29143,f770]) ).
fof(f29181,plain,
! [X0] :
( rR(sK1,sK3,X0)
| ~ ron(X0,vd1295)
| sK1 = X0
| vangle(sK3,sK1,sK3) = vangle(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f29162,f458]) ).
fof(f29187,plain,
! [X0] :
( rR(sK1,sK3,X0)
| ~ ron(X0,vd1295)
| sK1 = X0
| vangle(sK3,sK1,sK3) = vangle(sK3,sK1,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f29181,f462]) ).
fof(f29192,plain,
! [X0] :
( rR(sK1,sK3,X0)
| vd684 = vangle(sK3,sK1,X0)
| ~ ron(X0,vd1295)
| sK1 = X0
| ~ rpoint(X0) ),
inference(forward_demodulation,[],[f29187,f1827]) ).
fof(f29251,plain,
( ~ rR(sK3,sK1,vd1300)
| ~ rpoint(vd1300)
| ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ spl54_1294 ),
inference(resolution,[],[f24191,f795]) ).
fof(f29264,plain,
( ~ rR(sK3,sK1,vd1300)
| ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ spl54_1294 ),
inference(forward_subsumption_resolution,[],[f29251,f476]) ).
fof(f29272,plain,
( ~ rR(sK3,sK1,vd1300)
| ~ rpoint(sK1)
| ~ spl54_1294 ),
inference(forward_subsumption_resolution,[],[f29264,f458]) ).
fof(f29279,plain,
( ~ rR(sK3,sK1,vd1300)
| ~ spl54_1294 ),
inference(forward_subsumption_resolution,[],[f29272,f462]) ).
fof(f29283,plain,
( ~ spl54_1319
| ~ spl54_1294 ),
inference(avatar_split_clause,[],[f29279,f24190,f24320]) ).
fof(f29689,plain,
! [X0] :
( rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK1 = sK3
| sK3 = X0
| ~ ron(sK1,vd1297)
| vangle(sK1,sK3,sK1) = vangle(sK1,sK3,X0)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(resolution,[],[f27680,f1559]) ).
fof(f29693,plain,
! [X0] :
( rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK1 = sK3
| sK3 = X0
| ~ ron(sK1,vd1297)
| vangle(sK1,sK3,sK1) = vangle(sK1,sK3,X0)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(duplicate_literal_removal,[],[f29689]) ).
fof(f29716,plain,
! [X0] :
( rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK3 = X0
| ~ ron(sK1,vd1297)
| vangle(sK1,sK3,sK1) = vangle(sK1,sK3,X0)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f29693,f757]) ).
fof(f29738,plain,
! [X0] :
( rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK3 = X0
| vangle(sK1,sK3,sK1) = vangle(sK1,sK3,X0)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f29716,f768]) ).
fof(f29760,plain,
! [X0] :
( rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK3 = X0
| vangle(sK1,sK3,sK1) = vangle(sK1,sK3,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f29738,f462]) ).
fof(f29769,plain,
! [X0] :
( rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK3 = X0
| vangle(sK1,sK3,sK1) = vangle(sK1,sK3,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f29760,f458]) ).
fof(f29776,plain,
! [X0] :
( vd684 = vangle(sK1,sK3,X0)
| rR(sK3,sK1,X0)
| ~ ron(X0,vd1297)
| sK3 = X0
| ~ rpoint(X0) ),
inference(forward_demodulation,[],[f29769,f1900]) ).
fof(f29783,definition,
( spl54_1584
<=> ! [X0] :
( vd684 = vangle(sK1,sK3,X0)
| ~ rpoint(X0)
| sK3 = X0
| ~ ron(X0,vd1297)
| rR(sK3,sK1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_1584])],[avatar_definition]) ).
fof(f29784,plain,
( ! [X0] :
( rR(sK3,sK1,X0)
| ~ rpoint(X0)
| sK3 = X0
| ~ ron(X0,vd1297)
| vd684 = vangle(sK1,sK3,X0) )
| ~ spl54_1584 ),
inference(avatar_component_clause,[],[f29783]) ).
fof(f29788,plain,
spl54_1584,
inference(avatar_split_clause,[],[f29776,f29783]) ).
fof(f31928,plain,
! [X0,X1] :
( sK2 = X0
| X0 = X1
| sK3 = X0
| ~ rpoint(X0)
| rR(X0,sK3,sK2)
| ~ rpoint(X1)
| vangle(X1,X0,sK3) = vangle(X1,X0,sK2)
| ~ rpoint(sK3) ),
inference(resolution,[],[f28529,f772]) ).
fof(f31944,plain,
! [X0,X1] :
( ~ rpoint(X1)
| X0 = X1
| sK3 = X0
| ~ rpoint(X0)
| rR(X0,sK3,sK2)
| sK2 = X0
| vangle(X1,X0,sK3) = vangle(X1,X0,sK2) ),
inference(forward_subsumption_resolution,[],[f31928,f458]) ).
fof(f31945,plain,
( ~ rpoint(vd1300)
| vd1300 = sK3
| ~ ron(vd1300,vd1297)
| vd684 = vangle(sK1,sK3,vd1300)
| spl54_1319
| ~ spl54_1584 ),
inference(resolution,[],[f24322,f29784]) ).
fof(f31959,plain,
( vd1300 = sK3
| ~ ron(vd1300,vd1297)
| vd684 = vangle(sK1,sK3,vd1300)
| spl54_1319
| ~ spl54_1584 ),
inference(forward_subsumption_resolution,[],[f31945,f476]) ).
fof(f31965,plain,
( ~ ron(vd1300,vd1297)
| vd684 = vangle(sK1,sK3,vd1300)
| spl54_1319
| ~ spl54_1584 ),
inference(forward_subsumption_resolution,[],[f31959,f758]) ).
fof(f32421,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| X0 = X2
| X0 = X3
| ~ rpoint(X0)
| rR(X0,X3,X1)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,X3)
| ~ rpoint(X1)
| ~ rpoint(X3)
| X1 = X3
| ~ rpoint(X3)
| X1 = X3
| ~ rpoint(X1)
| ~ rpoint(X3) ),
inference(resolution,[],[f28512,f923]) ).
fof(f32433,plain,
! [X2,X3,X0,X1] :
( ~ rpoint(X3)
| X0 = X2
| X0 = X3
| ~ rpoint(X0)
| rR(X0,X3,X1)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,X3)
| ~ rpoint(X1)
| X0 = X1
| X1 = X3 ),
inference(duplicate_literal_removal,[],[f32421]) ).
fof(f32461,plain,
! [X2,X0,X1] :
( ~ rpoint(X2)
| sK1 = X0
| ~ rpoint(X0)
| rR(X0,sK1,X2)
| ~ rpoint(X1)
| vangle(X1,X0,X2) = vangle(X1,X0,sK1)
| X0 = X1
| X0 = X2
| sK1 = X2 ),
inference(resolution,[],[f32433,f462]) ).
fof(f32653,plain,
! [X0] :
( sK2 = X0
| sK3 = X0
| ~ rpoint(X0)
| rR(X0,sK3,sK2)
| sK2 = X0
| vangle(sK2,X0,sK2) = vangle(sK2,X0,sK3) ),
inference(resolution,[],[f31944,f460]) ).
fof(f32656,plain,
! [X0] :
( rR(X0,sK3,sK2)
| sK3 = X0
| ~ rpoint(X0)
| sK2 = X0
| vangle(sK2,X0,sK2) = vangle(sK2,X0,sK3) ),
inference(duplicate_literal_removal,[],[f32653]) ).
fof(f32685,plain,
( vd684 = vangle(sK1,sK3,vd1306)
| ~ ron(sK1,vd1297)
| ~ ron(sK3,vd1297)
| vd1306 = sK3
| sK1 = sK3
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(resolution,[],[f21856,f744]) ).
fof(f33114,plain,
( ~ rpoint(vd1303)
| vd1303 = sK3
| ~ ron(vd1303,vd1297)
| vangle(sK2,sK3,vd1303) = vangle(sK1,sK3,sK2)
| ~ spl54_1579 ),
inference(resolution,[],[f28660,f1676]) ).
fof(f33202,plain,
! [X0] :
( ~ ron(X0,vd1295)
| ~ ron(X0,vd1297)
| vd1297 = vd1295
| ~ rline(vd1297)
| sK3 = X0
| ~ rpoint(X0) ),
inference(resolution,[],[f21870,f770]) ).
fof(f33222,plain,
! [X0] :
( ~ ron(X0,vd1295)
| ~ ron(X0,vd1297)
| vd1297 = vd1295
| sK3 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f33202,f502]) ).
fof(f33226,definition,
( spl54_1615
<=> vd1297 = vd1295 ),
introduced(definition,[new_symbols(definition,[spl54_1615])],[avatar_definition]) ).
fof(f33228,plain,
( vd1297 = vd1295
| ~ spl54_1615 ),
inference(avatar_component_clause,[],[f33226]) ).
fof(f33230,definition,
( spl54_1616
<=> ! [X0] :
( ~ ron(X0,vd1295)
| ~ rpoint(X0)
| sK3 = X0
| ~ ron(X0,vd1297) ) ),
introduced(definition,[new_symbols(definition,[spl54_1616])],[avatar_definition]) ).
fof(f33231,plain,
( ! [X0] :
( ~ ron(X0,vd1295)
| ~ rpoint(X0)
| sK3 = X0
| ~ ron(X0,vd1297) )
| ~ spl54_1616 ),
inference(avatar_component_clause,[],[f33230]) ).
fof(f33232,plain,
( spl54_1615
| spl54_1616 ),
inference(avatar_split_clause,[],[f33222,f33230,f33226]) ).
fof(f33235,plain,
( ron(vd1300,vd1297)
| ~ spl54_1615 ),
inference(superposition,[],[f771,f33228]) ).
fof(f33242,plain,
( $false
| spl54_1566
| ~ spl54_1615 ),
inference(forward_subsumption_resolution,[],[f33235,f27412]) ).
fof(f33243,plain,
( spl54_1566
| ~ spl54_1615 ),
inference(avatar_contradiction_clause,[],[f33242]) ).
fof(f33247,plain,
( ~ rpoint(sK2)
| sK2 = sK3
| ~ ron(sK2,vd1297)
| ~ spl54_1616 ),
inference(resolution,[],[f33231,f769]) ).
fof(f34935,plain,
( sK1 = sK3
| ~ rpoint(sK1)
| sK1 = sK2
| vangle(sK2,sK1,sK2) = vangle(sK2,sK1,sK3)
| ~ rR(sK1,vd1303,sK2)
| ~ rpoint(sK2) ),
inference(resolution,[],[f32656,f2285]) ).
fof(f34949,plain,
( ~ rpoint(sK1)
| sK1 = sK2
| vangle(sK2,sK1,sK2) = vangle(sK2,sK1,sK3)
| ~ rR(sK1,vd1303,sK2)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f34935,f757]) ).
fof(f34957,plain,
( sK1 = sK2
| vangle(sK2,sK1,sK2) = vangle(sK2,sK1,sK3)
| ~ rR(sK1,vd1303,sK2)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f34949,f462]) ).
fof(f34964,plain,
( vangle(sK2,sK1,sK2) = vangle(sK2,sK1,sK3)
| ~ rR(sK1,vd1303,sK2)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f34957,f750]) ).
fof(f34968,plain,
( vangle(sK2,sK1,sK2) = vangle(sK2,sK1,sK3)
| ~ rR(sK1,vd1303,sK2) ),
inference(forward_subsumption_resolution,[],[f34964,f460]) ).
fof(f34971,plain,
( vangle(sK2,sK1,sK2) = vangle(sK3,sK1,sK2)
| ~ rR(sK1,vd1303,sK2) ),
inference(forward_demodulation,[],[f34968,f2149]) ).
fof(f34974,plain,
( vd684 = vangle(sK3,sK1,sK2)
| ~ rR(sK1,vd1303,sK2) ),
inference(forward_demodulation,[],[f34971,f1828]) ).
fof(f34976,plain,
( ~ rR(sK1,vd1303,sK2)
| spl54_1303 ),
inference(forward_subsumption_resolution,[],[f34974,f24238]) ).
fof(f34978,plain,
( ~ spl54_1564
| spl54_1303 ),
inference(avatar_split_clause,[],[f34976,f24236,f27312]) ).
fof(f37941,plain,
( sK2 = sK3
| ~ ron(sK2,vd1297)
| ~ spl54_1616 ),
inference(forward_subsumption_resolution,[],[f33247,f460]) ).
fof(f37964,plain,
( ~ ron(sK2,vd1297)
| ~ spl54_1616 ),
inference(forward_subsumption_resolution,[],[f37941,f761]) ).
fof(f37987,plain,
( $false
| ~ spl54_1554
| ~ spl54_1616 ),
inference(forward_subsumption_resolution,[],[f37964,f27047]) ).
fof(f37988,plain,
( ~ spl54_1554
| ~ spl54_1616 ),
inference(avatar_contradiction_clause,[],[f37987]) ).
fof(f40935,plain,
( ~ ron(sK1,vd1297)
| ~ ron(sK3,vd1297)
| vd1306 = sK3
| sK1 = sK3
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| spl54_1569 ),
inference(forward_subsumption_resolution,[],[f32685,f27436]) ).
fof(f40961,plain,
( ~ ron(sK3,vd1297)
| vd1306 = sK3
| sK1 = sK3
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| spl54_1569 ),
inference(forward_subsumption_resolution,[],[f40935,f768]) ).
fof(f40973,plain,
( vd1306 = sK3
| sK1 = sK3
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| spl54_1569 ),
inference(forward_subsumption_resolution,[],[f40961,f770]) ).
fof(f40985,plain,
( sK1 = sK3
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| spl54_1569 ),
inference(forward_subsumption_resolution,[],[f40973,f755]) ).
fof(f40996,plain,
( ~ rpoint(sK1)
| ~ rpoint(sK3)
| spl54_1569 ),
inference(forward_subsumption_resolution,[],[f40985,f757]) ).
fof(f41001,plain,
( ~ rpoint(sK3)
| spl54_1569 ),
inference(forward_subsumption_resolution,[],[f40996,f462]) ).
fof(f41007,plain,
( $false
| spl54_1569 ),
inference(forward_subsumption_resolution,[],[f41001,f458]) ).
fof(f41008,plain,
spl54_1569,
inference(avatar_contradiction_clause,[],[f41007]) ).
fof(f41362,plain,
( vd1303 = sK3
| ~ ron(vd1303,vd1297)
| vangle(sK2,sK3,vd1303) = vangle(sK1,sK3,sK2)
| ~ spl54_1579 ),
inference(forward_subsumption_resolution,[],[f33114,f455]) ).
fof(f41640,plain,
( ~ ron(vd1303,vd1297)
| vangle(sK2,sK3,vd1303) = vangle(sK1,sK3,sK2)
| spl54_23
| ~ spl54_1579 ),
inference(forward_subsumption_resolution,[],[f41362,f1908]) ).
fof(f41842,plain,
( vangle(sK2,sK3,vd1303) = vangle(sK1,sK3,sK2)
| spl54_23
| ~ spl54_1579 ),
inference(forward_subsumption_resolution,[],[f41640,f760]) ).
fof(f43220,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(vd1306,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) )
| spl54_13
| ~ spl54_1300 ),
inference(forward_subsumption_resolution,[],[f24026,f24223]) ).
fof(f44267,plain,
( ! [X0] :
( ~ ron(vd1306,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) )
| spl54_13
| ~ spl54_1300
| ~ spl54_1305 ),
inference(forward_subsumption_resolution,[],[f43220,f24246]) ).
fof(f44274,plain,
( vd684 != vf(sK1,vd1300)
| ~ rpoint(sK2)
| spl54_13 ),
inference(forward_subsumption_resolution,[],[f9104,f453]) ).
fof(f44285,plain,
( vd684 = vangle(sK1,sK3,vd1300)
| spl54_1319
| ~ spl54_1566
| ~ spl54_1584 ),
inference(forward_subsumption_resolution,[],[f31965,f27411]) ).
fof(f44309,plain,
( vd684 != vf(sK1,vd1300)
| spl54_13 ),
inference(forward_subsumption_resolution,[],[f44274,f460]) ).
fof(f44341,plain,
( vd684 != vf(sK1,sK1)
| spl54_13
| ~ spl54_15 ),
inference(forward_demodulation,[],[f44309,f1774]) ).
fof(f44348,plain,
( $false
| spl54_13
| ~ spl54_15 ),
inference(forward_subsumption_resolution,[],[f44341,f1651]) ).
fof(f44349,plain,
( spl54_13
| ~ spl54_15 ),
inference(avatar_contradiction_clause,[],[f44348]) ).
fof(f44434,plain,
( vangle(vd1300,sK3,sK1) = vangle(sK1,sK3,vd1300)
| spl54_15 ),
inference(forward_subsumption_resolution,[],[f8891,f1773]) ).
fof(f44938,plain,
( ~ rline(vd1297)
| ~ ron(sK1,vd1297)
| ~ spl54_1293 ),
inference(resolution,[],[f24188,f770]) ).
fof(f45411,plain,
( ~ ron(sK1,vd1297)
| ~ spl54_1293 ),
inference(forward_subsumption_resolution,[],[f44938,f502]) ).
fof(f45429,plain,
( $false
| ~ spl54_1293 ),
inference(forward_subsumption_resolution,[],[f45411,f768]) ).
fof(f45430,plain,
~ spl54_1293,
inference(avatar_contradiction_clause,[],[f45429]) ).
fof(f46652,plain,
( vd684 != sF52
| ~ spl54_1295 ),
inference(superposition,[],[f1556,f24195]) ).
fof(f47234,plain,
( vd684 = vangle(sK3,sK1,vd1300)
| ~ ron(vd1300,vd1295)
| vd1300 = sK1
| ~ rpoint(vd1300)
| spl54_1294 ),
inference(resolution,[],[f24192,f29192]) ).
fof(f47245,plain,
( vd684 = vangle(sK3,sK1,vd1300)
| vd1300 = sK1
| ~ rpoint(vd1300)
| spl54_1294 ),
inference(forward_subsumption_resolution,[],[f47234,f771]) ).
fof(f47251,plain,
( vd684 = vangle(sK3,sK1,vd1300)
| ~ rpoint(vd1300)
| spl54_15
| spl54_1294 ),
inference(forward_subsumption_resolution,[],[f47245,f1773]) ).
fof(f47257,plain,
( vd684 = vangle(sK3,sK1,vd1300)
| spl54_15
| spl54_1294 ),
inference(forward_subsumption_resolution,[],[f47251,f476]) ).
fof(f47263,plain,
( vd684 = sF53
| spl54_15
| spl54_1294 ),
inference(forward_demodulation,[],[f47257,f1555]) ).
fof(f47497,plain,
( ! [X0] :
( vd684 != vd684
| ron(vd1306,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| vd1306 = sK3
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(vd1306)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1569 ),
inference(superposition,[],[f957,f27437]) ).
fof(f47498,plain,
( ! [X0] :
( ron(vd1306,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| vd1306 = sK3
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(vd1306)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1569 ),
inference(trivial_inequality_removal,[],[f47497]) ).
fof(f48679,plain,
( ! [X0] :
( ron(vd1306,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(vd1306)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1569 ),
inference(forward_subsumption_resolution,[],[f47498,f755]) ).
fof(f48698,plain,
( ! [X0] :
( ron(vd1306,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(vd1306)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1569 ),
inference(forward_subsumption_resolution,[],[f48679,f757]) ).
fof(f48714,plain,
( ! [X0] :
( ron(vd1306,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1569 ),
inference(forward_subsumption_resolution,[],[f48698,f453]) ).
fof(f48726,plain,
( ! [X0] :
( ron(vd1306,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK3) )
| ~ spl54_1569 ),
inference(forward_subsumption_resolution,[],[f48714,f462]) ).
fof(f48731,plain,
( ! [X0] :
( ron(vd1306,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) )
| ~ spl54_1569 ),
inference(forward_subsumption_resolution,[],[f48726,f458]) ).
fof(f49010,plain,
( ~ rline(vd1297)
| ~ ron(sK1,vd1297)
| ron(sK2,vd1297)
| ~ spl54_1333 ),
inference(resolution,[],[f24530,f770]) ).
fof(f49854,plain,
! [X0,X1] :
( sK1 = X0
| ~ rpoint(X0)
| rR(X0,sK1,sK2)
| ~ rpoint(X1)
| vangle(X1,X0,sK2) = vangle(X1,X0,sK1)
| X0 = X1
| sK2 = X0
| sK1 = sK2 ),
inference(resolution,[],[f32461,f460]) ).
fof(f49857,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| rR(X0,sK1,sK2)
| sK1 = X0
| vangle(X1,X0,sK2) = vangle(X1,X0,sK1)
| X0 = X1
| sK2 = X0 ),
inference(forward_subsumption_resolution,[],[f49854,f750]) ).
fof(f49890,plain,
! [X0] :
( ~ rpoint(X0)
| rR(X0,sK1,sK2)
| sK1 = X0
| vangle(sK2,X0,sK2) = vangle(sK2,X0,sK1)
| sK2 = X0
| sK2 = X0 ),
inference(resolution,[],[f49857,f460]) ).
fof(f49892,plain,
! [X0] :
( rR(X0,sK1,sK2)
| ~ rpoint(X0)
| sK1 = X0
| vangle(sK2,X0,sK2) = vangle(sK2,X0,sK1)
| sK2 = X0 ),
inference(duplicate_literal_removal,[],[f49890]) ).
fof(f49912,plain,
( ~ rpoint(sK3)
| sK1 = sK3
| vangle(sK2,sK3,sK1) = vangle(sK2,sK3,sK2)
| sK2 = sK3
| rR(sK1,vd1303,sK2)
| ~ rpoint(sK2) ),
inference(resolution,[],[f49892,f1738]) ).
fof(f49923,plain,
( sK1 = sK3
| vangle(sK2,sK3,sK1) = vangle(sK2,sK3,sK2)
| sK2 = sK3
| rR(sK1,vd1303,sK2)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f49912,f458]) ).
fof(f49935,plain,
( vangle(sK2,sK3,sK1) = vangle(sK2,sK3,sK2)
| sK2 = sK3
| rR(sK1,vd1303,sK2)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f49923,f757]) ).
fof(f49947,plain,
( vangle(sK2,sK3,sK1) = vangle(sK2,sK3,sK2)
| rR(sK1,vd1303,sK2)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f49935,f761]) ).
fof(f51181,plain,
( vd684 = vangle(sK2,sK3,vd1303)
| ~ ron(sK2,vd1297)
| ~ ron(sK3,vd1297)
| vd1303 = sK3
| sK2 = sK3
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| rR(sK2,vd1300,vd1303)
| ~ rpoint(vd1303) ),
inference(resolution,[],[f21863,f1739]) ).
fof(f54222,plain,
! [X2,X3,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X2
| ~ ron(X2,sK13(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,[],[f3889,f1066]) ).
fof(f54244,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,sK13(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,[],[f54222]) ).
fof(f54323,plain,
! [X0] :
( ~ rpoint(sK3)
| sK1 = sK2
| ~ rpoint(sK1)
| sK1 = sK3
| rR(sK3,sK1,sK2)
| ~ ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2) ),
inference(resolution,[],[f54244,f5852]) ).
fof(f54982,plain,
( $false
| spl54_15
| spl54_1294
| spl54_1295 ),
inference(forward_subsumption_resolution,[],[f47263,f24196]) ).
fof(f54983,plain,
( spl54_15
| spl54_1294
| spl54_1295 ),
inference(avatar_contradiction_clause,[],[f54982]) ).
fof(f55242,plain,
( vd684 = vangle(sK2,sK3,vd1303)
| ~ ron(sK3,vd1297)
| vd1303 = sK3
| sK2 = sK3
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| rR(sK2,vd1300,vd1303)
| ~ rpoint(vd1303)
| ~ spl54_1554 ),
inference(forward_subsumption_resolution,[],[f51181,f27047]) ).
fof(f55514,plain,
( vd684 = vangle(sK2,sK3,vd1303)
| vd1303 = sK3
| sK2 = sK3
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| rR(sK2,vd1300,vd1303)
| ~ rpoint(vd1303)
| ~ spl54_1554 ),
inference(forward_subsumption_resolution,[],[f55242,f770]) ).
fof(f55684,plain,
( vd684 = vangle(sK2,sK3,vd1303)
| sK2 = sK3
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| rR(sK2,vd1300,vd1303)
| ~ rpoint(vd1303)
| spl54_23
| ~ spl54_1554 ),
inference(forward_subsumption_resolution,[],[f55514,f1908]) ).
fof(f55787,plain,
( vd684 = vangle(sK2,sK3,vd1303)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| rR(sK2,vd1300,vd1303)
| ~ rpoint(vd1303)
| spl54_23
| ~ spl54_1554 ),
inference(forward_subsumption_resolution,[],[f55684,f761]) ).
fof(f55858,plain,
( vd684 = vangle(sK2,sK3,vd1303)
| ~ rpoint(sK3)
| rR(sK2,vd1300,vd1303)
| ~ rpoint(vd1303)
| spl54_23
| ~ spl54_1554 ),
inference(forward_subsumption_resolution,[],[f55787,f460]) ).
fof(f55904,plain,
( vd684 = vangle(sK2,sK3,vd1303)
| rR(sK2,vd1300,vd1303)
| ~ rpoint(vd1303)
| spl54_23
| ~ spl54_1554 ),
inference(forward_subsumption_resolution,[],[f55858,f458]) ).
fof(f55935,plain,
( vd684 = vangle(sK2,sK3,vd1303)
| ~ rpoint(vd1303)
| spl54_23
| ~ spl54_1554
| ~ spl54_1572 ),
inference(forward_subsumption_resolution,[],[f55904,f27928]) ).
fof(f55951,plain,
( vd684 = vangle(sK2,sK3,vd1303)
| spl54_23
| ~ spl54_1554
| ~ spl54_1572 ),
inference(forward_subsumption_resolution,[],[f55935,f455]) ).
fof(f55962,plain,
( vd684 = vangle(sK1,sK3,sK2)
| spl54_23
| ~ spl54_1554
| ~ spl54_1572
| ~ spl54_1579 ),
inference(forward_demodulation,[],[f55951,f41842]) ).
fof(f55971,plain,
( $false
| spl54_23
| spl54_1300
| ~ spl54_1554
| ~ spl54_1572
| ~ spl54_1579 ),
inference(forward_subsumption_resolution,[],[f55962,f24224]) ).
fof(f55972,plain,
( spl54_23
| spl54_1300
| ~ spl54_1554
| ~ spl54_1572
| ~ spl54_1579 ),
inference(avatar_contradiction_clause,[],[f55971]) ).
fof(f55985,plain,
( $false
| ~ spl54_1295
| ~ spl54_1320 ),
inference(forward_subsumption_resolution,[],[f46652,f24385]) ).
fof(f55986,plain,
( ~ spl54_1295
| ~ spl54_1320 ),
inference(avatar_contradiction_clause,[],[f55985]) ).
fof(f56205,plain,
( ~ ron(sK1,vd1297)
| ron(sK2,vd1297)
| ~ spl54_1333 ),
inference(forward_subsumption_resolution,[],[f49010,f502]) ).
fof(f56218,plain,
( vangle(sK2,sK3,sK1) = vangle(sK2,sK3,sK2)
| ~ rpoint(sK2)
| spl54_1564 ),
inference(forward_subsumption_resolution,[],[f49947,f27313]) ).
fof(f56355,plain,
( ron(sK2,vd1297)
| ~ spl54_1333 ),
inference(forward_subsumption_resolution,[],[f56205,f768]) ).
fof(f56363,plain,
( vangle(sK2,sK3,sK1) = vangle(sK2,sK3,sK2)
| spl54_1564 ),
inference(forward_subsumption_resolution,[],[f56218,f460]) ).
fof(f56444,plain,
( $false
| ~ spl54_1333
| spl54_1554 ),
inference(forward_subsumption_resolution,[],[f56355,f27048]) ).
fof(f56445,plain,
( ~ spl54_1333
| spl54_1554 ),
inference(avatar_contradiction_clause,[],[f56444]) ).
fof(f56453,plain,
( vd684 = vangle(sK2,sK3,sK1)
| spl54_1564 ),
inference(forward_demodulation,[],[f56363,f1899]) ).
fof(f56492,plain,
( vd684 = vangle(sK1,sK3,sK2)
| spl54_1564 ),
inference(forward_demodulation,[],[f56453,f2178]) ).
fof(f56516,plain,
( $false
| spl54_1300
| spl54_1564 ),
inference(forward_subsumption_resolution,[],[f56492,f24224]) ).
fof(f56517,plain,
( spl54_1300
| spl54_1564 ),
inference(avatar_contradiction_clause,[],[f56516]) ).
fof(f56578,definition,
( spl54_1824
<=> vd684 = vangle(sK1,sK3,vd1300) ),
introduced(definition,[new_symbols(definition,[spl54_1824])],[avatar_definition]) ).
fof(f56580,plain,
( vd684 = vangle(sK1,sK3,vd1300)
| ~ spl54_1824 ),
inference(avatar_component_clause,[],[f56578]) ).
fof(f56587,plain,
( spl54_1824
| spl54_1319
| ~ spl54_1566
| ~ spl54_1584 ),
inference(avatar_split_clause,[],[f44285,f29783,f27410,f24320,f56578]) ).
fof(f56729,plain,
( ! [X0] :
( ~ rpoint(sK3)
| sK1 = sK2
| ~ rpoint(sK1)
| sK1 = sK3
| rR(sK3,sK1,sK2)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2) )
| ~ spl54_1307 ),
inference(forward_subsumption_resolution,[],[f54323,f24254]) ).
fof(f56841,plain,
( vangle(sK2,sK3,sK1) = vangle(sK1,sK3,vd1300)
| spl54_15 ),
inference(forward_demodulation,[],[f44434,f742]) ).
fof(f57049,plain,
( ! [X0] :
( sK1 = sK2
| ~ rpoint(sK1)
| sK1 = sK3
| rR(sK3,sK1,sK2)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2) )
| ~ spl54_1307 ),
inference(forward_subsumption_resolution,[],[f56729,f458]) ).
fof(f57148,plain,
( vangle(sK1,sK3,sK2) = vangle(sK1,sK3,vd1300)
| spl54_15 ),
inference(forward_demodulation,[],[f56841,f2178]) ).
fof(f57321,plain,
( ! [X0] :
( ~ rpoint(sK1)
| sK1 = sK3
| rR(sK3,sK1,sK2)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2) )
| ~ spl54_1307 ),
inference(forward_subsumption_resolution,[],[f57049,f750]) ).
fof(f57475,plain,
( ! [X0] :
( sK1 = sK3
| rR(sK3,sK1,sK2)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2) )
| ~ spl54_1307 ),
inference(forward_subsumption_resolution,[],[f57321,f462]) ).
fof(f57573,plain,
( ! [X0] :
( rR(sK3,sK1,sK2)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2) )
| ~ spl54_1307 ),
inference(forward_subsumption_resolution,[],[f57475,f757]) ).
fof(f57640,plain,
( ! [X0] :
( ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2) )
| ~ spl54_1307
| spl54_1346 ),
inference(forward_subsumption_resolution,[],[f57573,f24687]) ).
fof(f57690,plain,
( ! [X0] :
( ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) )
| ~ spl54_1307
| spl54_1346 ),
inference(forward_subsumption_resolution,[],[f57640,f460]) ).
fof(f57715,plain,
( spl54_1305
| ~ spl54_1307
| spl54_1346 ),
inference(avatar_split_clause,[],[f57690,f24685,f24253,f24245]) ).
fof(f59790,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) )
| spl54_13
| ~ spl54_1300
| ~ spl54_1305
| ~ spl54_1569 ),
inference(forward_subsumption_resolution,[],[f48731,f44267]) ).
fof(f60030,plain,
( spl54_1293
| spl54_13
| ~ spl54_1300
| ~ spl54_1305
| ~ spl54_1569 ),
inference(avatar_split_clause,[],[f59790,f27435,f24245,f24222,f1747,f24187]) ).
fof(f60644,plain,
( ! [X0] :
( vd684 != vd684
| ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| sK1 = sK2
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_1303 ),
inference(superposition,[],[f957,f24237]) ).
fof(f60645,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| sK1 = sK2
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_1303 ),
inference(trivial_inequality_removal,[],[f60644]) ).
fof(f60850,plain,
( ! [X0] :
( vd684 != vd684
| ~ rR(sK3,sK1,sK2)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| sK2 = sK3
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1300 ),
inference(superposition,[],[f953,f24223]) ).
fof(f60853,plain,
( ! [X0] :
( ~ rR(sK3,sK1,sK2)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| sK2 = sK3
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1300 ),
inference(trivial_inequality_removal,[],[f60850]) ).
fof(f60894,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| sK2 = sK3
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1300
| ~ spl54_1346 ),
inference(forward_subsumption_resolution,[],[f60853,f24686]) ).
fof(f60899,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1300
| ~ spl54_1346 ),
inference(forward_subsumption_resolution,[],[f60894,f761]) ).
fof(f60903,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1300
| ~ spl54_1346 ),
inference(forward_subsumption_resolution,[],[f60899,f757]) ).
fof(f60905,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1300
| ~ spl54_1346 ),
inference(forward_subsumption_resolution,[],[f60903,f460]) ).
fof(f60906,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK3) )
| ~ spl54_1300
| ~ spl54_1346 ),
inference(forward_subsumption_resolution,[],[f60905,f462]) ).
fof(f60907,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) )
| ~ spl54_1300
| ~ spl54_1346 ),
inference(forward_subsumption_resolution,[],[f60906,f458]) ).
fof(f60908,plain,
( spl54_1293
| ~ spl54_1300
| ~ spl54_1346 ),
inference(avatar_split_clause,[],[f60907,f24685,f24222,f24187]) ).
fof(f60969,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_1303 ),
inference(forward_subsumption_resolution,[],[f60645,f750]) ).
fof(f60990,plain,
( vd684 = vangle(sK1,sK3,sK2)
| spl54_15
| ~ spl54_1824 ),
inference(forward_demodulation,[],[f57148,f56580]) ).
fof(f61082,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_1303 ),
inference(forward_subsumption_resolution,[],[f60969,f757]) ).
fof(f61104,plain,
( $false
| spl54_15
| spl54_1300
| ~ spl54_1824 ),
inference(forward_subsumption_resolution,[],[f60990,f24224]) ).
fof(f61105,plain,
( spl54_15
| spl54_1300
| ~ spl54_1824 ),
inference(avatar_contradiction_clause,[],[f61104]) ).
fof(f61169,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_1303 ),
inference(forward_subsumption_resolution,[],[f61082,f460]) ).
fof(f61189,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK1) )
| ~ spl54_1303 ),
inference(forward_subsumption_resolution,[],[f61169,f458]) ).
fof(f61204,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0) )
| ~ spl54_1303 ),
inference(forward_subsumption_resolution,[],[f61189,f462]) ).
fof(f61210,plain,
( spl54_1333
| ~ spl54_1303 ),
inference(avatar_split_clause,[],[f61204,f24236,f24529]) ).
cnf(s15,plain,
( spl54_15
| ~ spl54_16 ),
inference(sat_conversion,[],[f1779]) ).
cnf(s25,plain,
( ~ spl54_13
| ~ spl54_15 ),
inference(sat_conversion,[],[f1972]) ).
cnf(s27,plain,
( ~ spl54_13
| spl54_16 ),
inference(sat_conversion,[],[f1988]) ).
cnf(s33,plain,
~ spl54_23,
inference(sat_conversion,[],[f2123]) ).
cnf(s1318,plain,
( ~ spl54_1300
| spl54_1307 ),
inference(sat_conversion,[],[f24255]) ).
cnf(s1643,plain,
( spl54_13
| spl54_1320
| spl54_1572 ),
inference(sat_conversion,[],[f27910]) ).
cnf(s1651,plain,
spl54_1579,
inference(sat_conversion,[],[f28665]) ).
cnf(s1658,plain,
( ~ spl54_1294
| ~ spl54_1319 ),
inference(sat_conversion,[],[f29283]) ).
cnf(s1665,plain,
spl54_1584,
inference(sat_conversion,[],[f29788]) ).
cnf(s1696,plain,
( spl54_1615
| spl54_1616 ),
inference(sat_conversion,[],[f33232]) ).
cnf(s1697,plain,
( spl54_1566
| ~ spl54_1615 ),
inference(sat_conversion,[],[f33243]) ).
cnf(s1738,plain,
( spl54_1303
| ~ spl54_1564 ),
inference(sat_conversion,[],[f34978]) ).
cnf(s1852,plain,
( ~ spl54_1554
| ~ spl54_1616 ),
inference(sat_conversion,[],[f37988]) ).
cnf(s1947,plain,
spl54_1569,
inference(sat_conversion,[],[f41008]) ).
cnf(s2032,plain,
( spl54_13
| ~ spl54_15 ),
inference(sat_conversion,[],[f44349]) ).
cnf(s2089,plain,
~ spl54_1293,
inference(sat_conversion,[],[f45430]) ).
cnf(s2210,plain,
( spl54_15
| spl54_1294
| spl54_1295 ),
inference(sat_conversion,[],[f54983]) ).
cnf(s2281,plain,
( spl54_23
| spl54_1300
| ~ spl54_1554
| ~ spl54_1572
| ~ spl54_1579 ),
inference(sat_conversion,[],[f55972]) ).
cnf(s2286,plain,
( ~ spl54_1295
| ~ spl54_1320 ),
inference(sat_conversion,[],[f55986]) ).
cnf(s2296,plain,
( ~ spl54_1333
| spl54_1554 ),
inference(sat_conversion,[],[f56445]) ).
cnf(s2299,plain,
( spl54_1300
| spl54_1564 ),
inference(sat_conversion,[],[f56517]) ).
cnf(s2305,plain,
( spl54_1319
| ~ spl54_1566
| ~ spl54_1584
| spl54_1824 ),
inference(sat_conversion,[],[f56587]) ).
cnf(s2352,plain,
( spl54_1305
| ~ spl54_1307
| spl54_1346 ),
inference(sat_conversion,[],[f57715]) ).
cnf(s2618,plain,
( spl54_13
| spl54_1293
| ~ spl54_1300
| ~ spl54_1305
| ~ spl54_1569 ),
inference(sat_conversion,[],[f60030]) ).
cnf(s2651,plain,
( spl54_1293
| ~ spl54_1300
| ~ spl54_1346 ),
inference(sat_conversion,[],[f60908]) ).
cnf(s2682,plain,
( spl54_15
| spl54_1300
| ~ spl54_1824 ),
inference(sat_conversion,[],[f61105]) ).
cnf(s2704,plain,
( ~ spl54_1303
| spl54_1333 ),
inference(sat_conversion,[],[f61210]) ).
cnf(s2887,plain,
( ~ spl54_1300
| spl54_13 ),
inference(rat,[],[s2352,s2618,s1318,s2651,s2089,s1947]) ).
cnf(s2888,plain,
spl54_13,
inference(rat,[],[s1658,s2305,s2210,s2286,s1697,s1643,s1696,s2281,s1852,s2296,s2704,s1738,s2299,s2682,s2887,s2032,s1665,s33,s1651]) ).
cnf(s2889,plain,
spl54_16,
inference(rat,[],[s27,s2888]) ).
cnf(s2890,plain,
~ spl54_15,
inference(rat,[],[s25,s2888]) ).
cnf(s2893,plain,
$false,
inference(rat,[],[s15,s2889,s2890]) ).
fof(f61213,plain,
$false,
inference(avatar_sat_refutation,[],[s2893]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO311+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n026.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 08:06:11 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.06/2.11 % (2512264)Detected formulas, will run a generic FOF schedule.
% 10.06/2.11 % (2512274)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=68817406:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.06/2.11 % (2512271)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=2527366722:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.06/2.11 % (2512273)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4109019160:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.06/2.11 % (2512272)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3605189894:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.06/2.11 % (2512269)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=225342423:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.06/2.11 % (2512270)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=3298183087:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.06/2.11 % (2512275)dis-21_1_sil=8000:lcm=predicate:random_seed=3722624476:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.06/2.11 % (2512274)Instruction limit reached!
% 10.06/2.11 % (2512274)------------------------------
% 10.06/2.11 % (2512274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.11 % (2512274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.11 % (2512274)CaDiCaL version: 2.1.3
% 10.06/2.11 % (2512274)Termination reason: Instruction limit
% 10.06/2.11 % (2512274)Termination phase: Saturation
% 10.06/2.11 % (2512274)Time elapsed: 0.047 s
% 10.06/2.11 % (2512274)Peak memory usage: 90 MB
% 10.06/2.11 % (2512274)Instructions burned: 141 (million)
% 10.06/2.11 % (2512272)Instruction limit reached!
% 10.06/2.11 % (2512272)------------------------------
% 10.06/2.11 % (2512272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.11 % (2512272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.11 % (2512272)CaDiCaL version: 2.1.3
% 10.06/2.11 % (2512272)Termination reason: Instruction limit
% 10.06/2.11 % (2512272)Termination phase: Saturation
% 10.06/2.11 % (2512272)Time elapsed: 0.055 s
% 10.06/2.11 % (2512272)Peak memory usage: 89 MB
% 10.06/2.11 % (2512272)Instructions burned: 109 (million)
% 10.06/2.11 % (2512273)Instruction limit reached!
% 10.06/2.11 % (2512273)------------------------------
% 10.06/2.11 % (2512273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.11 % (2512273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.11 % (2512273)CaDiCaL version: 2.1.3
% 10.06/2.11 % (2512273)Termination reason: Instruction limit
% 10.06/2.11 % (2512273)Termination phase: Saturation
% 10.06/2.11 % (2512273)Time elapsed: 0.063 s
% 10.06/2.11 % (2512273)Peak memory usage: 88 MB
% 10.06/2.11 % (2512273)Instructions burned: 120 (million)
% 10.06/2.11 % (2512275)Instruction limit reached!
% 10.06/2.11 % (2512275)------------------------------
% 10.06/2.11 % (2512275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.11 % (2512275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.11 % (2512275)CaDiCaL version: 2.1.3
% 10.06/2.11 % (2512275)Termination reason: Instruction limit
% 10.06/2.11 % (2512275)Termination phase: Saturation
% 10.06/2.11 % (2512275)Time elapsed: 0.070 s
% 10.06/2.11 % (2512275)Peak memory usage: 90 MB
% 10.06/2.11 % (2512275)Instructions burned: 131 (million)
% 10.06/2.11 % (2512283)lrs+10_1_sil=8000:sp=occurrence:random_seed=1782499967:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.06/2.11 % (2512283)Instruction limit reached!
% 10.06/2.11 % (2512283)------------------------------
% 10.06/2.11 % (2512283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.11 % (2512283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.11 % (2512283)CaDiCaL version: 2.1.3
% 10.06/2.11 % (2512283)Termination reason: Instruction limit
% 10.06/2.11 % (2512283)Termination phase: Saturation
% 10.06/2.11 % (2512283)Time elapsed: 0.081 s
% 10.06/2.11 % (2512283)Peak memory usage: 92 MB
% 10.06/2.11 % (2512283)Instructions burned: 287 (million)
% 15.23/2.89 % (2512284)lrs+10_1_sil=32000:urr=on:br=off:random_seed=751745725:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 15.23/2.89 % (2512285)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3038272707:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 15.23/2.89 % (2512286)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=270429039:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 15.23/2.89 % (2512284)Instruction limit reached!
% 15.23/2.89 % (2512284)------------------------------
% 15.23/2.89 % (2512284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.23/2.89 % (2512284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.23/2.89 % (2512284)CaDiCaL version: 2.1.3
% 15.23/2.89 % (2512284)Termination reason: Instruction limit
% 15.23/2.89 % (2512284)Termination phase: Saturation
% 15.23/2.89 % (2512284)Time elapsed: 0.074 s
% 15.23/2.89 % (2512284)Peak memory usage: 90 MB
% 15.23/2.89 % (2512284)Instructions burned: 157 (million)
% 15.23/2.89 % (2512289)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1022675656:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 15.23/2.89 % (2512289)Refutation not found, incomplete strategy
% 15.23/2.89 % (2512289)------------------------------
% 15.23/2.89 % (2512289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.23/2.89 % (2512289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.23/2.89 % (2512289)CaDiCaL version: 2.1.3
% 15.23/2.89 % (2512289)Termination reason: Refutation not found, incomplete strategy
% 15.23/2.89 % (2512289)Time elapsed: 0.011 s
% 15.23/2.89 % (2512289)Peak memory usage: 89 MB
% 15.23/2.89 % (2512289)Instructions burned: 40 (million)
% 15.23/2.89 % (2512286)Instruction limit reached!
% 15.23/2.89 % (2512286)------------------------------
% 15.23/2.89 % (2512286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.23/2.89 % (2512286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.23/2.89 % (2512286)CaDiCaL version: 2.1.3
% 15.23/2.89 % (2512286)Termination reason: Instruction limit
% 15.23/2.89 % (2512286)Termination phase: Saturation
% 15.23/2.89 % (2512286)Time elapsed: 0.121 s
% 15.23/2.89 % (2512286)Peak memory usage: 93 MB
% 15.23/2.89 % (2512286)Instructions burned: 248 (million)
% 15.23/2.89 % (2512285)Instruction limit reached!
% 15.23/2.89 % (2512285)------------------------------
% 15.23/2.89 % (2512285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.23/2.89 % (2512285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.23/2.89 % (2512285)CaDiCaL version: 2.1.3
% 15.23/2.89 % (2512285)Termination reason: Instruction limit
% 15.23/2.89 % (2512285)Termination phase: Saturation
% 15.23/2.89 % (2512285)Time elapsed: 0.155 s
% 15.23/2.89 % (2512285)Peak memory usage: 90 MB
% 15.23/2.89 % (2512285)Instructions burned: 328 (million)
% 15.23/2.89 % (2512292)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1649504828:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 15.23/2.89 % (2512289)------------------------------
% 15.23/2.89 % (2512289)------------------------------
% 15.23/2.89 % (2512294)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1102732784:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 15.23/2.89 % (2512295)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2909531332:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 15.23/2.89 % (2512294)Instruction limit reached!
% 15.23/2.89 % (2512294)------------------------------
% 15.23/2.89 % (2512294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.23/2.89 % (2512294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.23/2.89 % (2512294)CaDiCaL version: 2.1.3
% 15.23/2.89 % (2512294)Termination reason: Instruction limit
% 15.23/2.89 % (2512294)Termination phase: Saturation
% 15.23/2.89 % (2512294)Time elapsed: 0.060 s
% 15.23/2.89 % (2512294)Peak memory usage: 90 MB
% 15.23/2.89 % (2512294)Instructions burned: 114 (million)
% 15.23/2.89 % (2512295)Refutation not found, incomplete strategy
% 15.23/2.89 % (2512295)------------------------------
% 15.23/2.89 % (2512295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.23/2.89 % (2512295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.56/4.83 % (2512295)CaDiCaL version: 2.1.3
% 29.56/4.83 % (2512295)Termination reason: Refutation not found, incomplete strategy
% 29.56/4.83 % (2512295)Time elapsed: 0.026 s
% 29.56/4.83 % (2512295)Peak memory usage: 89 MB
% 29.56/4.83 % (2512295)Instructions burned: 53 (million)
% 29.56/4.83 % (2512297)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3586846264:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 29.56/4.83 % (2512297)Instruction limit reached!
% 29.56/4.83 % (2512297)------------------------------
% 29.56/4.83 % (2512297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.56/4.83 % (2512297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.56/4.83 % (2512297)CaDiCaL version: 2.1.3
% 29.56/4.83 % (2512297)Termination reason: Instruction limit
% 29.56/4.83 % (2512297)Termination phase: Saturation
% 29.56/4.83 % (2512297)Time elapsed: 0.026 s
% 29.56/4.83 % (2512297)Peak memory usage: 89 MB
% 29.56/4.83 % (2512297)Instructions burned: 119 (million)
% 29.56/4.83 % (2512302)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=8849732:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi)
% 29.56/4.83 % (2512300)lrs+10_1_sil=8000:sp=occurrence:random_seed=329697430:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 29.56/4.83 % (2512302)Refutation not found, incomplete strategy
% 29.56/4.83 % (2512302)------------------------------
% 29.56/4.83 % (2512302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.56/4.83 % (2512302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.56/4.83 % (2512302)CaDiCaL version: 2.1.3
% 29.56/4.83 % (2512302)Termination reason: Refutation not found, incomplete strategy
% 29.56/4.83 % (2512302)Time elapsed: 0.009 s
% 29.56/4.83 % (2512302)Peak memory usage: 89 MB
% 29.56/4.83 % (2512302)Instructions burned: 32 (million)
% 29.56/4.83 % (2512295)------------------------------
% 29.56/4.83 % (2512295)------------------------------
% 29.56/4.83 % (2512302)------------------------------
% 29.56/4.83 % (2512302)------------------------------
% 29.56/4.83 % (2512306)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2895061590:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2990 on theBenchmark for (2990ds/134Mi)
% 29.56/4.83 % (2512305)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2987450899:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 29.56/4.83 % (2512306)Instruction limit reached!
% 29.56/4.83 % (2512306)------------------------------
% 29.56/4.83 % (2512306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.56/4.83 % (2512306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.56/4.83 % (2512306)CaDiCaL version: 2.1.3
% 29.56/4.83 % (2512306)Termination reason: Instruction limit
% 29.56/4.83 % (2512306)Termination phase: Saturation
% 29.56/4.83 % (2512306)Time elapsed: 0.036 s
% 29.56/4.83 % (2512306)Peak memory usage: 93 MB
% 29.56/4.83 % (2512306)Instructions burned: 138 (million)
% 29.56/4.83 % (2512309)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3396937772:st=8:i=592:sd=3:ep=RST:ss=axioms_2989 on theBenchmark for (2989ds/592Mi)
% 29.56/4.83 % (2512300)Instruction limit reached!
% 29.56/4.83 % (2512300)------------------------------
% 29.56/4.83 % (2512300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.56/4.83 % (2512300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.56/4.83 % (2512300)CaDiCaL version: 2.1.3
% 29.56/4.83 % (2512300)Termination reason: Instruction limit
% 29.56/4.83 % (2512300)Termination phase: Saturation
% 29.56/4.83 % (2512300)Time elapsed: 0.482 s
% 29.56/4.83 % (2512300)Peak memory usage: 98 MB
% 29.56/4.83 % (2512300)Instructions burned: 908 (million)
% 29.56/4.83 % (2512311)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=579476864:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 29.56/4.83 % (2512309)Instruction limit reached!
% 29.56/4.83 % (2512309)------------------------------
% 29.56/4.83 % (2512309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.56/4.83 % (2512309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.56/4.83 % (2512309)CaDiCaL version: 2.1.3
% 29.56/4.83 % (2512309)Termination reason: Instruction limit
% 29.56/4.83 % (2512309)Termination phase: Saturation
% 29.56/4.83 % (2512309)Time elapsed: 0.287 s
% 29.56/4.83 % (2512309)Peak memory usage: 92 MB
% 29.56/4.83 % (2512309)Instructions burned: 592 (million)
% 44.34/7.92 % (2512313)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=3603100373:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 44.34/7.92 % (2512292)Instruction limit reached!
% 44.34/7.92 % (2512292)------------------------------
% 44.34/7.92 % (2512292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512292)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512292)Termination reason: Instruction limit
% 44.34/7.92 % (2512292)Termination phase: Saturation
% 44.34/7.92 % (2512292)Time elapsed: 1.079 s
% 44.34/7.92 % (2512292)Peak memory usage: 141 MB
% 44.34/7.92 % (2512292)Instructions burned: 2351 (million)
% 44.34/7.92 % (2512313)Instruction limit reached!
% 44.34/7.92 % (2512313)------------------------------
% 44.34/7.92 % (2512313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512313)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512313)Termination reason: Instruction limit
% 44.34/7.92 % (2512313)Termination phase: Saturation
% 44.34/7.92 % (2512313)Time elapsed: 0.066 s
% 44.34/7.92 % (2512313)Peak memory usage: 91 MB
% 44.34/7.92 % (2512313)Instructions burned: 126 (million)
% 44.34/7.92 % (2512315)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3905224204:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 44.34/7.92 % (2512315)Instruction limit reached!
% 44.34/7.92 % (2512315)------------------------------
% 44.34/7.92 % (2512315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512315)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512315)Termination reason: Instruction limit
% 44.34/7.92 % (2512315)Termination phase: Saturation
% 44.34/7.92 % (2512315)Time elapsed: 0.042 s
% 44.34/7.92 % (2512315)Peak memory usage: 91 MB
% 44.34/7.92 % (2512315)Instructions burned: 134 (million)
% 44.34/7.92 % (2512316)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1337384375:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 44.34/7.92 % (2512316)Refutation not found, incomplete strategy
% 44.34/7.92 % (2512316)------------------------------
% 44.34/7.92 % (2512316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512316)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512316)Termination reason: Refutation not found, incomplete strategy
% 44.34/7.92 % (2512316)Time elapsed: 0.013 s
% 44.34/7.92 % (2512316)Peak memory usage: 89 MB
% 44.34/7.92 % (2512316)Instructions burned: 26 (million)
% 44.34/7.92 % (2512318)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2816122527:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi)
% 44.34/7.92 % (2512318)Refutation not found, incomplete strategy
% 44.34/7.92 % (2512318)------------------------------
% 44.34/7.92 % (2512318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512318)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512318)Termination reason: Refutation not found, incomplete strategy
% 44.34/7.92 % (2512318)Time elapsed: 0.004 s
% 44.34/7.92 % (2512318)Peak memory usage: 88 MB
% 44.34/7.92 % (2512318)Instructions burned: 11 (million)
% 44.34/7.92 % (2512318)------------------------------
% 44.34/7.92 % (2512318)------------------------------
% 44.34/7.92 % (2512316)------------------------------
% 44.34/7.92 % (2512316)------------------------------
% 44.34/7.92 % (2512321)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=3284507729:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi)
% 44.34/7.92 % (2512322)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=3545725341:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2979 on theBenchmark for (2979ds/150Mi)
% 44.34/7.92 % (2512322)Instruction limit reached!
% 44.34/7.92 % (2512322)------------------------------
% 44.34/7.92 % (2512322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512322)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512322)Termination reason: Instruction limit
% 44.34/7.92 % (2512322)Termination phase: Saturation
% 44.34/7.92 % (2512322)Time elapsed: 0.076 s
% 44.34/7.92 % (2512322)Peak memory usage: 92 MB
% 44.34/7.92 % (2512322)Instructions burned: 150 (million)
% 44.34/7.92 % (2512325)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1861621764:i=14155:bd=all_2977 on theBenchmark for (2977ds/14155Mi)
% 44.34/7.92 % (2512321)Instruction limit reached!
% 44.34/7.92 % (2512321)------------------------------
% 44.34/7.92 % (2512321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512321)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512321)Termination reason: Instruction limit
% 44.34/7.92 % (2512321)Termination phase: Saturation
% 44.34/7.92 % (2512321)Time elapsed: 1.625 s
% 44.34/7.92 % (2512321)Peak memory usage: 141 MB
% 44.34/7.92 % (2512321)Instructions burned: 6064 (million)
% 44.34/7.92 % (2512327)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3203442968:i=667:av=off:fsr=off_2962 on theBenchmark for (2962ds/667Mi)
% 44.34/7.92 % (2512327)Refutation not found, incomplete strategy
% 44.34/7.92 % (2512327)------------------------------
% 44.34/7.92 % (2512327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512327)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512327)Termination reason: Refutation not found, incomplete strategy
% 44.34/7.92 % (2512327)Time elapsed: 0.012 s
% 44.34/7.92 % (2512327)Peak memory usage: 89 MB
% 44.34/7.92 % (2512327)Instructions burned: 44 (million)
% 44.34/7.92 % (2512305)Instruction limit reached!
% 44.34/7.92 % (2512305)------------------------------
% 44.34/7.92 % (2512305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512305)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512305)Termination reason: Instruction limit
% 44.34/7.92 % (2512305)Termination phase: Saturation
% 44.34/7.92 % (2512305)Time elapsed: 2.800 s
% 44.34/7.92 % (2512305)Peak memory usage: 142 MB
% 44.34/7.92 % (2512305)Instructions burned: 5205 (million)
% 44.34/7.92 % (2512327)------------------------------
% 44.34/7.92 % (2512327)------------------------------
% 44.34/7.92 % (2512329)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=448104385:s2a=on:i=185:s2at=1.8:fdi=4_2961 on theBenchmark for (2961ds/185Mi)
% 44.34/7.92 % (2512330)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2457182572:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2960 on theBenchmark for (2960ds/193Mi)
% 44.34/7.92 % (2512329)Instruction limit reached!
% 44.34/7.92 % (2512329)------------------------------
% 44.34/7.92 % (2512329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512329)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512329)Termination reason: Instruction limit
% 44.34/7.92 % (2512329)Termination phase: Saturation
% 44.34/7.92 % (2512329)Time elapsed: 0.098 s
% 44.34/7.92 % (2512329)Peak memory usage: 93 MB
% 44.34/7.92 % (2512329)Instructions burned: 186 (million)
% 44.34/7.92 % (2512330)Instruction limit reached!
% 44.34/7.92 % (2512330)------------------------------
% 44.34/7.92 % (2512330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512330)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512330)Termination reason: Instruction limit
% 44.34/7.92 % (2512330)Termination phase: Saturation
% 44.34/7.92 % (2512330)Time elapsed: 0.057 s
% 44.34/7.92 % (2512330)Peak memory usage: 91 MB
% 44.34/7.92 % (2512330)Instructions burned: 196 (million)
% 44.34/7.92 % (2512334)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2085053621:i=12111:sd=1:ss=included_2958 on theBenchmark for (2958ds/12111Mi)
% 44.34/7.92 % (2512333)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4003089437:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2959 on theBenchmark for (2959ds/4850Mi)
% 44.34/7.92 % (2512333)Refutation not found, incomplete strategy
% 44.34/7.92 % (2512333)------------------------------
% 44.34/7.92 % (2512333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512333)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512333)Termination reason: Refutation not found, incomplete strategy
% 44.34/7.92 % (2512333)Time elapsed: 0.017 s
% 44.34/7.92 % (2512333)Peak memory usage: 89 MB
% 44.34/7.92 % (2512333)Instructions burned: 32 (million)
% 44.34/7.92 % (2512333)------------------------------
% 44.34/7.92 % (2512333)------------------------------
% 44.34/7.92 % (2512337)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3868665393:i=319:kws=precedence:fsr=off_2955 on theBenchmark for (2955ds/319Mi)
% 44.34/7.92 % (2512337)Instruction limit reached!
% 44.34/7.92 % (2512337)------------------------------
% 44.34/7.92 % (2512337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512337)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512337)Termination reason: Instruction limit
% 44.34/7.92 % (2512337)Termination phase: Saturation
% 44.34/7.92 % (2512337)Time elapsed: 0.162 s
% 44.34/7.92 % (2512337)Peak memory usage: 94 MB
% 44.34/7.92 % (2512337)Instructions burned: 320 (million)
% 44.34/7.92 % (2512339)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3965040412:i=2064:ep=RST_2952 on theBenchmark for (2952ds/2064Mi)
% 44.34/7.92 % (2512339)Instruction limit reached!
% 44.34/7.92 % (2512339)------------------------------
% 44.34/7.92 % (2512339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.92 % (2512339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.92 % (2512339)CaDiCaL version: 2.1.3
% 44.34/7.92 % (2512339)Termination reason: Instruction limit
% 44.34/7.92 % (2512339)Termination phase: Saturation
% 44.34/7.92 % (2512339)Time elapsed: 0.968 s
% 44.34/7.93 % (2512339)Peak memory usage: 96 MB
% 44.34/7.93 % (2512339)Instructions burned: 2065 (million)
% 44.34/7.93 % (2512341)dis-1011_128_sil=32000:random_seed=997520677:i=3706:ep=RST:av=off_2941 on theBenchmark for (2941ds/3706Mi)
% 44.34/7.93 % (2512269)First to succeed.
% 44.34/7.93 % (2512269)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2512264"
% 44.34/7.93 % (2512341)Instruction limit reached!
% 44.34/7.93 % (2512341)------------------------------
% 44.34/7.93 % (2512341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.93 % (2512341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.93 % (2512341)CaDiCaL version: 2.1.3
% 44.34/7.93 % (2512341)Termination reason: Instruction limit
% 44.34/7.93 % (2512341)Termination phase: Saturation
% 44.34/7.93 % (2512341)Time elapsed: 1.253 s
% 44.34/7.93 % (2512341)Peak memory usage: 89 MB
% 44.34/7.93 % (2512341)Instructions burned: 3708 (million)
% 44.34/7.93 % (2512269)Refutation found. Thanks to Tanya!
% 44.34/7.93 % SZS status Theorem for theBenchmark
% 44.34/7.93 % SZS output start Proof for theBenchmark
% See solution above
% 44.34/8.02 % (2512269)------------------------------
% 44.34/8.02 % (2512269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/8.02 % (2512269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/8.02 % (2512269)CaDiCaL version: 2.1.3
% 44.34/8.02 % (2512269)Termination reason: Refutation
% 44.34/8.02 % (2512269)Time elapsed: 6.868 s
% 44.34/8.02 % (2512269)Peak memory usage: 184 MB
% 44.34/8.02 % (2512269)Instructions burned: 11807 (million)
% 44.34/8.02 % (2512269)------------------------------
% 44.34/8.02 % (2512269)------------------------------
% 44.34/8.02 % (2512264)Success in time 7.29 s
% 44.34/8.02 % Vampire exiting
%------------------------------------------------------------------------------