%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO328+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 : n009.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:28 AM UTC 2026
% Result : Theorem 35.60s 5.98s
% Output : Refutation 36.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 81
% Syntax : Number of formulae : 756 ( 122 unt; 41 def)
% Number of atoms : 4140 ( 950 equ)
% Maximal formula atoms : 26 ( 5 avg)
% Number of connectives : 5979 (2595 ~;3158 |; 168 &)
% ( 45 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 45 ( 43 usr; 40 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 16 con; 0-3 aty)
% Number of variables : 1020 ( 0 sgn 972 !; 48 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vangle(vd1289,vd1288,vd1302) = vangle(vd1288,vd1289,vd1329),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(378), 1349, 0)') ).
fof(f2,negated_conjecture,
vangle(vd1289,vd1288,vd1302) != vangle(vd1288,vd1289,vd1329),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
vangle(vd1302,vd1289,vd1288) = vangle(vd1329,vd1288,vd1289),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(378), 1348, 0)') ).
fof(f4,axiom,
vf(vd1288,vd1329) = vf(vd1289,vd1302),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(377, 1347, 0)') ).
fof(f5,axiom,
vangle(vd1289,vd1302,vd1288) = vangle(vd1288,vd1329,vd1289),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(376), 1346, 0)') ).
fof(f8,axiom,
vf(vd1302,vd1288) = vf(vd1329,vd1289),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(375), 1343, 0)') ).
fof(f9,axiom,
vangle(vd1287,vd1302,vd1288) = vangle(vd1287,vd1329,vd1289),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(375)), 1344, 0)') ).
fof(f10,axiom,
vangle(vd1289,vd1287,vd1288) = vangle(vd1302,vd1287,vd1288),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(374, 1342, 0)') ).
fof(f14,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(f15,axiom,
vangle(vd1289,vd1287,vd1288) = vangle(vd1289,vd1287,vd1329),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(373, 1341, 0)') ).
fof(f16,axiom,
~ rR(vd1287,vd1288,vd1329),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','neg(neg(conjunct2(372)))') ).
fof(f17,axiom,
~ rR(vd1287,vd1289,vd1302),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','neg(neg(372))') ).
fof(f19,axiom,
rpoint(vd1329),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(367, 0)') ).
fof(f21,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(f23,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(f27,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(f28,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(f34,axiom,
vd1329 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(368)), 1332, 0)') ).
fof(f39,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(f41,axiom,
vd1289 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(371)), 1338, 0)') ).
fof(f43,axiom,
vd1302 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(conjunct2(conjunct2(368))), 1334, 0)') ).
fof(f78,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(f79,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(f80,axiom,
vd1288 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(371), 1337, 0)') ).
fof(f81,axiom,
ron(vd1329,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(s2(plural(370)), 0)') ).
fof(f83,axiom,
vd1329 != vd1302,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(conjunct2(368))), 1333, 0)') ).
fof(f84,axiom,
ron(vd1302,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct2(349), 0)') ).
fof(f86,axiom,
ron(vd1289,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(s2(plural(347)), 0)') ).
fof(f88,axiom,
rline(vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(347, 0)') ).
fof(f89,axiom,
ron(vd1288,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(s2(plural(346)), 0)') ).
fof(f91,axiom,
rline(vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(346, 0)') ).
fof(f93,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(f94,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(f99,axiom,
ron(vd1287,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(s2(plural(369)), 0)') ).
fof(f100,axiom,
ron(vd1287,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(s1(plural(369)), 0)') ).
fof(f108,axiom,
! [X0,X1,X2,X3,X4] :
( ( X3 = X4
& ron(X2,X3)
& ron(X1,X3)
& ron(X0,X3)
& rline(X4)
& X1 != X2
& X0 != X2
& X0 != X1
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(91), 0), imp(cond(axiom(91), 0)))') ).
fof(f109,axiom,
! [X0,X1,X2,X3,X4] :
( ( X3 = X4
& ron(X1,X3)
& ron(X0,X3)
& rR(X1,X0,X2)
& rline(X4)
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ron(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(83), 0), imp(cond(axiom(83), 0)))') ).
fof(f111,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(f117,axiom,
v0 = vd684,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(axiom(137), 2)') ).
fof(f119,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(f144,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(f188,plain,
vangle(vd1289,vd1288,vd1302) != vangle(vd1288,vd1289,vd1329),
inference(flattening,[],[f2]) ).
fof(f199,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,[],[f14]) ).
fof(f200,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,[],[f199]) ).
fof(f207,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,[],[f27]) ).
fof(f208,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,[],[f207]) ).
fof(f209,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,[],[f28]) ).
fof(f210,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,[],[f209]) ).
fof(f223,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,[],[f39]) ).
fof(f224,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,[],[f223]) ).
fof(f260,plain,
! [X0,X1] :
( ( vf(X0,X1) = v0
<=> X0 = X1 )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f78]) ).
fof(f261,plain,
! [X0,X1] :
( ( vf(X0,X1) = v0
<=> X0 = X1 )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f260]) ).
fof(f262,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,[],[f79]) ).
fof(f263,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,[],[f262]) ).
fof(f266,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,[],[f93]) ).
fof(f267,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,[],[f266]) ).
fof(f268,plain,
! [X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f94]) ).
fof(f269,plain,
! [X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f268]) ).
fof(f290,plain,
! [X0,X1,X2,X3,X4] :
( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f108]) ).
fof(f291,plain,
! [X0,X1,X2,X3,X4] :
( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f290]) ).
fof(f292,plain,
! [X0,X1,X2,X3,X4] :
( ron(X2,X3)
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f109]) ).
fof(f293,plain,
! [X0,X1,X2,X3,X4] :
( ron(X2,X3)
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f292]) ).
fof(f296,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,[],[f111]) ).
fof(f297,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,[],[f296]) ).
fof(f308,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,[],[f119]) ).
fof(f309,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,[],[f308]) ).
fof(f357,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,[],[f144]) ).
fof(f358,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,[],[f357]) ).
fof(f439,plain,
( vf(vd1287,vd1288) = vf(vd1287,vd1289)
& vd1288 != vd1289
& vd1287 != vd1289
& vd1287 != vd1288
& vd1289 = sK4
& rpoint(sK4)
& vd1288 = sK5
& rpoint(sK5)
& vd1287 = sK6
& rpoint(sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6)],[f23]) ).
fof(f445,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,[],[f261]) ).
fof(f446,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,[],[f263]) ).
fof(f447,plain,
! [X0,X1] :
( ( ron(X1,sK7(X0,X1))
& ron(X0,sK7(X0,X1))
& rline(sK7(X0,X1)) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f446]) ).
fof(f452,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
| v0 != vangle(X2,X0,X4) )
& ( 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,[],[f267]) ).
fof(f453,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
| v0 != vangle(X2,X0,X4) )
& ( 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,[],[f452]) ).
fof(f512,plain,
vangle(vd1289,vd1288,vd1302) != vangle(vd1288,vd1289,vd1329),
inference(cnf_transformation,[],[f188]) ).
fof(f513,plain,
vangle(vd1302,vd1289,vd1288) = vangle(vd1329,vd1288,vd1289),
inference(cnf_transformation,[],[f3]) ).
fof(f514,plain,
vf(vd1288,vd1329) = vf(vd1289,vd1302),
inference(cnf_transformation,[],[f4]) ).
fof(f515,plain,
vangle(vd1289,vd1302,vd1288) = vangle(vd1288,vd1329,vd1289),
inference(cnf_transformation,[],[f5]) ).
fof(f518,plain,
vf(vd1302,vd1288) = vf(vd1329,vd1289),
inference(cnf_transformation,[],[f8]) ).
fof(f519,plain,
vangle(vd1287,vd1302,vd1288) = vangle(vd1287,vd1329,vd1289),
inference(cnf_transformation,[],[f9]) ).
fof(f520,plain,
vangle(vd1289,vd1287,vd1288) = vangle(vd1302,vd1287,vd1288),
inference(cnf_transformation,[],[f10]) ).
fof(f533,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,[],[f200]) ).
fof(f534,plain,
vangle(vd1289,vd1287,vd1288) = vangle(vd1289,vd1287,vd1329),
inference(cnf_transformation,[],[f15]) ).
fof(f535,plain,
~ rR(vd1287,vd1288,vd1329),
inference(cnf_transformation,[],[f16]) ).
fof(f536,plain,
~ rR(vd1287,vd1289,vd1302),
inference(cnf_transformation,[],[f17]) ).
fof(f538,plain,
rpoint(vd1329),
inference(cnf_transformation,[],[f19]) ).
fof(f541,plain,
rpoint(vd1303),
inference(cnf_transformation,[],[f21]) ).
fof(f542,plain,
rR(vd1289,vd1287,vd1302),
inference(cnf_transformation,[],[f21]) ).
fof(f543,plain,
vd1302 = vd1303,
inference(cnf_transformation,[],[f21]) ).
fof(f545,plain,
rpoint(sK6),
inference(cnf_transformation,[],[f439]) ).
fof(f546,plain,
vd1287 = sK6,
inference(cnf_transformation,[],[f439]) ).
fof(f547,plain,
rpoint(sK5),
inference(cnf_transformation,[],[f439]) ).
fof(f548,plain,
vd1288 = sK5,
inference(cnf_transformation,[],[f439]) ).
fof(f549,plain,
rpoint(sK4),
inference(cnf_transformation,[],[f439]) ).
fof(f550,plain,
vd1289 = sK4,
inference(cnf_transformation,[],[f439]) ).
fof(f553,plain,
vd1289 != vd1288,
inference(cnf_transformation,[],[f439]) ).
fof(f558,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,[],[f208]) ).
fof(f559,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,[],[f210]) ).
fof(f560,plain,
! [X2,X3,X0,X1,X4,X5] :
( X0 != X1
| ~ rR(X1,X0,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(cnf_transformation,[],[f210]) ).
fof(f562,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,[],[f210]) ).
fof(f569,plain,
vd1329 != vd1287,
inference(cnf_transformation,[],[f34]) ).
fof(f574,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,[],[f224]) ).
fof(f576,plain,
vd1289 != vd1287,
inference(cnf_transformation,[],[f41]) ).
fof(f578,plain,
vd1302 != vd1287,
inference(cnf_transformation,[],[f43]) ).
fof(f615,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| vf(X0,X1) != v0
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f445]) ).
fof(f616,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = v0
| X0 != X1
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f445]) ).
fof(f617,plain,
! [X3,X0,X1,X4] :
( rline(sK7(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f447]) ).
fof(f618,plain,
! [X3,X0,X1,X4] :
( ron(X0,sK7(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f447]) ).
fof(f619,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK7(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f447]) ).
fof(f620,plain,
vd1288 != vd1287,
inference(cnf_transformation,[],[f80]) ).
fof(f621,plain,
ron(vd1329,vd1295),
inference(cnf_transformation,[],[f81]) ).
fof(f623,plain,
vd1302 != vd1329,
inference(cnf_transformation,[],[f83]) ).
fof(f624,plain,
ron(vd1302,vd1297),
inference(cnf_transformation,[],[f84]) ).
fof(f626,plain,
ron(vd1289,vd1297),
inference(cnf_transformation,[],[f86]) ).
fof(f628,plain,
rline(vd1297),
inference(cnf_transformation,[],[f88]) ).
fof(f629,plain,
ron(vd1288,vd1295),
inference(cnf_transformation,[],[f89]) ).
fof(f631,plain,
rline(vd1295),
inference(cnf_transformation,[],[f91]) ).
fof(f648,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( v0 = vangle(X2,X0,X4)
| 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,[],[f453]) ).
fof(f649,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X4,X6)
| v0 != vangle(X2,X0,X4)
| ~ 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,[],[f453]) ).
fof(f650,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rR(X0,X2,X4)
| v0 != vangle(X2,X0,X4)
| ~ 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,[],[f453]) ).
fof(f651,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f269]) ).
fof(f656,plain,
ron(vd1287,vd1297),
inference(cnf_transformation,[],[f99]) ).
fof(f657,plain,
ron(vd1287,vd1295),
inference(cnf_transformation,[],[f100]) ).
fof(f669,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f291]) ).
fof(f670,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X2,X3)
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f293]) ).
fof(f672,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,[],[f297]) ).
fof(f686,plain,
v0 = vd684,
inference(cnf_transformation,[],[f117]) ).
fof(f688,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,[],[f309]) ).
fof(f730,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,[],[f358]) ).
fof(f842,plain,
vangle(sK4,sK5,vd1303) != vangle(sK5,sK4,vd1329),
inference(definition_unfolding,[],[f512,f550,f548,f543,f548,f550]) ).
fof(f843,plain,
vangle(vd1303,sK4,sK5) = vangle(vd1329,sK5,sK4),
inference(definition_unfolding,[],[f513,f543,f550,f548,f548,f550]) ).
fof(f844,plain,
vf(sK5,vd1329) = vf(sK4,vd1303),
inference(definition_unfolding,[],[f514,f548,f550,f543]) ).
fof(f845,plain,
vangle(sK4,vd1303,sK5) = vangle(sK5,vd1329,sK4),
inference(definition_unfolding,[],[f515,f550,f543,f548,f548,f550]) ).
fof(f848,plain,
vf(vd1303,sK5) = vf(vd1329,sK4),
inference(definition_unfolding,[],[f518,f543,f548,f550]) ).
fof(f849,plain,
vangle(sK6,vd1303,sK5) = vangle(sK6,vd1329,sK4),
inference(definition_unfolding,[],[f519,f546,f543,f548,f546,f550]) ).
fof(f850,plain,
vangle(sK4,sK6,sK5) = vangle(vd1303,sK6,sK5),
inference(definition_unfolding,[],[f520,f550,f546,f548,f543,f546,f548]) ).
fof(f851,plain,
vangle(sK4,sK6,sK5) = vangle(sK4,sK6,vd1329),
inference(definition_unfolding,[],[f534,f550,f546,f548,f550,f546]) ).
fof(f852,plain,
~ rR(sK6,sK5,vd1329),
inference(definition_unfolding,[],[f535,f546,f548]) ).
fof(f853,plain,
~ rR(sK6,sK4,vd1303),
inference(definition_unfolding,[],[f536,f546,f550,f543]) ).
fof(f855,plain,
rR(sK4,sK6,vd1303),
inference(definition_unfolding,[],[f542,f550,f546,f543]) ).
fof(f858,plain,
sK4 != sK5,
inference(definition_unfolding,[],[f553,f550,f548]) ).
fof(f863,plain,
vd1329 != sK6,
inference(definition_unfolding,[],[f569,f546]) ).
fof(f865,plain,
sK4 != sK6,
inference(definition_unfolding,[],[f576,f550,f546]) ).
fof(f867,plain,
vd1303 != sK6,
inference(definition_unfolding,[],[f578,f543,f546]) ).
fof(f900,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = vd684
| X0 != X1
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(definition_unfolding,[],[f616,f686]) ).
fof(f901,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| vf(X0,X1) != vd684
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(definition_unfolding,[],[f615,f686]) ).
fof(f902,plain,
sK5 != sK6,
inference(definition_unfolding,[],[f620,f548,f546]) ).
fof(f904,plain,
vd1329 != vd1303,
inference(definition_unfolding,[],[f623,f543]) ).
fof(f905,plain,
ron(vd1303,vd1297),
inference(definition_unfolding,[],[f624,f543]) ).
fof(f907,plain,
ron(sK4,vd1297),
inference(definition_unfolding,[],[f626,f550]) ).
fof(f909,plain,
ron(sK5,vd1295),
inference(definition_unfolding,[],[f629,f548]) ).
fof(f911,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,[],[f650,f686]) ).
fof(f912,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,[],[f649,f686]) ).
fof(f913,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,[],[f648,f686]) ).
fof(f915,plain,
ron(sK6,vd1297),
inference(definition_unfolding,[],[f656,f546]) ).
fof(f916,plain,
ron(sK6,vd1295),
inference(definition_unfolding,[],[f657,f546]) ).
fof(f993,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,[],[f533]) ).
fof(f994,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,[],[f993]) ).
fof(f995,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,[],[f994]) ).
fof(f996,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,[],[f995]) ).
fof(f997,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,[],[f996]) ).
fof(f998,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,[],[f997]) ).
fof(f999,plain,
! [X10,X11,X8,X9,X7,X12,X13] :
( vangle(X10,X13,X9) = vangle(X12,X13,X11)
| 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)
| ~ ron(X13,X8)
| ~ rline(X7)
| ~ rline(X8)
| ~ rpoint(X9)
| ~ rpoint(X10)
| ~ rpoint(X11)
| ~ rpoint(X12)
| ~ rpoint(X13) ),
inference(equality_resolution,[],[f998]) ).
fof(f1012,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,[],[f558]) ).
fof(f1013,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,[],[f1012]) ).
fof(f1014,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,[],[f1013]) ).
fof(f1015,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,[],[f1014]) ).
fof(f1016,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,[],[f562]) ).
fof(f1017,plain,
! [X3,X0,X4,X5] :
( ~ rR(X0,X4,X3)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1016]) ).
fof(f1018,plain,
! [X3,X4,X5] :
( ~ rR(X5,X4,X3)
| ~ rR(X4,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1017]) ).
fof(f1023,plain,
! [X2,X3,X1,X4,X5] :
( ~ rR(X1,X1,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X1 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f560]) ).
fof(f1024,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X1,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X1 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1023]) ).
fof(f1025,plain,
! [X3,X4,X5] :
( ~ rR(X4,X4,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X4 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1024]) ).
fof(f1026,plain,
! [X3,X5] :
( ~ rR(X5,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1025]) ).
fof(f1027,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,[],[f559]) ).
fof(f1028,plain,
! [X3,X0,X4,X5] :
( rR(X4,X3,X0)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1027]) ).
fof(f1029,plain,
! [X3,X4,X5] :
( ~ rR(X4,X5,X3)
| rR(X4,X3,X5)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1028]) ).
fof(f1052,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,[],[f574]) ).
fof(f1053,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,[],[f1052]) ).
fof(f1054,plain,
! [X3,X4,X5] :
( vangle(X3,X4,X5) = vangle(X5,X4,X3)
| X3 = X5
| X4 = X5
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1053]) ).
fof(f1076,plain,
! [X2,X3,X1] :
( vd684 = vf(X1,X1)
| X1 != X2
| ~ rpoint(X2)
| X1 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f900]) ).
fof(f1077,plain,
! [X2,X3] :
( vd684 = vf(X2,X2)
| ~ rpoint(X2)
| X2 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f1076]) ).
fof(f1078,plain,
! [X3] :
( vd684 = vf(X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f1077]) ).
fof(f1079,plain,
! [X2,X3,X0] :
( X0 = X2
| vf(X0,X2) != vd684
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f901]) ).
fof(f1080,plain,
! [X2,X3] :
( vd684 != vf(X3,X2)
| X2 = X3
| ~ rpoint(X2)
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f1079]) ).
fof(f1081,plain,
! [X3,X0,X4] :
( ron(X3,sK7(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f619]) ).
fof(f1082,plain,
! [X3,X4] :
( ron(X3,sK7(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1081]) ).
fof(f1083,plain,
! [X3,X0,X4] :
( ron(X0,sK7(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f618]) ).
fof(f1084,plain,
! [X3,X4] :
( ron(X4,sK7(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1083]) ).
fof(f1085,plain,
! [X3,X0,X4] :
( rline(sK7(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f617]) ).
fof(f1086,plain,
! [X3,X4] :
( rline(sK7(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1085]) ).
fof(f1121,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,[],[f911]) ).
fof(f1122,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,[],[f1121]) ).
fof(f1123,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,[],[f1122]) ).
fof(f1124,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,[],[f1123]) ).
fof(f1125,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,[],[f912]) ).
fof(f1126,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,[],[f1125]) ).
fof(f1127,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,[],[f1126]) ).
fof(f1128,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,[],[f1127]) ).
fof(f1129,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,[],[f913]) ).
fof(f1130,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,[],[f1129]) ).
fof(f1131,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,[],[f1130]) ).
fof(f1132,plain,
! [X3,X1,X7,X5] :
( vd684 = vangle(X3,X1,X5)
| rR(X1,X3,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,[],[f1131]) ).
fof(f1133,plain,
! [X2,X3,X0] :
( vf(X0,X2) = vf(X2,X0)
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f651]) ).
fof(f1134,plain,
! [X2,X3] :
( vf(X3,X2) = vf(X2,X3)
| ~ rpoint(X2)
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f1133]) ).
fof(f1171,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1)
| ~ ron(X2,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f669]) ).
fof(f1172,plain,
! [X0,X1,X6,X7,X4,X5] :
( rR(X1,X0,X5)
| rR(X0,X1,X5)
| rR(X5,X0,X1)
| ~ ron(X5,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rline(X4)
| X1 = X5
| X0 = X5
| X0 = X1
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1171]) ).
fof(f1173,plain,
! [X0,X6,X7,X4,X5] :
( rR(X6,X0,X5)
| rR(X0,X6,X5)
| rR(X5,X0,X6)
| ~ ron(X5,X4)
| ~ ron(X6,X4)
| ~ ron(X0,X4)
| ~ rline(X4)
| X5 = X6
| X0 = X5
| X0 = X6
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1172]) ).
fof(f1174,plain,
! [X6,X7,X4,X5] :
( rR(X7,X6,X5)
| rR(X6,X7,X5)
| rR(X5,X7,X6)
| ~ ron(X5,X4)
| ~ ron(X6,X4)
| ~ ron(X7,X4)
| ~ rline(X4)
| X5 = X6
| X5 = X7
| X6 = X7
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1173]) ).
fof(f1175,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ron(X2,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f670]) ).
fof(f1176,plain,
! [X0,X1,X6,X7,X4,X5] :
( ron(X5,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rR(X1,X0,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1175]) ).
fof(f1177,plain,
! [X0,X6,X7,X4,X5] :
( ron(X5,X4)
| ~ ron(X6,X4)
| ~ ron(X0,X4)
| ~ rR(X6,X0,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1176]) ).
fof(f1178,plain,
! [X6,X7,X4,X5] :
( ~ rR(X6,X7,X5)
| ~ ron(X6,X4)
| ~ ron(X7,X4)
| ron(X5,X4)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1177]) ).
fof(f1181,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,[],[f672]) ).
fof(f1182,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,[],[f1181]) ).
fof(f1183,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,[],[f1182]) ).
fof(f1184,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,[],[f1183]) ).
fof(f1211,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,[],[f688]) ).
fof(f1212,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,[],[f1211]) ).
fof(f1213,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,[],[f1212]) ).
fof(f1214,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,[],[f1213]) ).
fof(f1369,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,[],[f730]) ).
fof(f1370,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,[],[f1369]) ).
fof(f1371,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,[],[f1370]) ).
fof(f1372,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,[],[f1371]) ).
fof(f1691,definition,
sF52 = vangle(sK4,sK5,vd1303),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f1692,plain,
vangle(sK4,sK5,vd1303) = sF52,
inference(reorient_equations,[],[f1691]) ).
fof(f1693,definition,
sF53 = vangle(sK5,sK4,vd1329),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f1694,plain,
vangle(sK5,sK4,vd1329) = sF53,
inference(reorient_equations,[],[f1693]) ).
fof(f1695,plain,
sF52 != sF53,
inference(definition_folding,[],[f842,f1694,f1692]) ).
fof(f1696,plain,
! [X3] :
( vd684 = vf(X3,X3)
| ~ rpoint(X3) ),
inference(duplicate_literal_removal,[],[f1078]) ).
fof(f1697,plain,
! [X3,X5] :
( ~ rR(X5,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X5) ),
inference(duplicate_literal_removal,[],[f1026]) ).
fof(f1787,definition,
( spl54_21
<=> sK4 = sK6 ),
introduced(definition,[new_symbols(definition,[spl54_21])],[avatar_definition]) ).
fof(f1789,plain,
( sK4 != sK6
| spl54_21 ),
inference(avatar_component_clause,[],[f1787]) ).
fof(f1864,plain,
~ spl54_21,
inference(avatar_split_clause,[],[f865,f1787]) ).
fof(f1865,plain,
vangle(vd1303,sK6,sK5) = vangle(sK4,sK6,vd1329),
inference(backward_demodulation,[],[f851,f850]) ).
fof(f1867,plain,
( rR(sK4,vd1303,sK6)
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(resolution,[],[f1029,f855]) ).
fof(f1868,plain,
( rR(sK4,vd1303,sK6)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1867,f541]) ).
fof(f1869,plain,
( rR(sK4,vd1303,sK6)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1868,f549]) ).
fof(f1870,plain,
rR(sK4,vd1303,sK6),
inference(forward_subsumption_resolution,[],[f1869,f545]) ).
fof(f1920,plain,
vd684 = vf(vd1329,vd1329),
inference(unit_resulting_resolution,[],[f1696,f538]) ).
fof(f1922,plain,
vd684 = vf(vd1303,vd1303),
inference(unit_resulting_resolution,[],[f1696,f541]) ).
fof(f1936,plain,
vf(sK5,vd1329) = vf(vd1329,sK5),
inference(unit_resulting_resolution,[],[f1134,f547,f538]) ).
fof(f1947,plain,
vf(sK4,vd1303) = vf(vd1303,sK4),
inference(unit_resulting_resolution,[],[f1134,f549,f541]) ).
fof(f1973,plain,
vf(sK4,vd1303) = vf(vd1329,sK5),
inference(backward_demodulation,[],[f844,f1936]) ).
fof(f1982,plain,
vf(vd1329,sK5) = vf(vd1303,sK4),
inference(backward_demodulation,[],[f1947,f1973]) ).
fof(f2020,plain,
~ rR(vd1303,vd1303,sK6),
inference(unit_resulting_resolution,[],[f1697,f541,f545]) ).
fof(f2076,plain,
vd684 = vangle(sK5,sK6,vd1329),
inference(unit_resulting_resolution,[],[f1132,f545,f547,f538,f631,f902,f863,f916,f909,f852,f621]) ).
fof(f2107,plain,
vangle(vd1303,sK6,vd1329) = vangle(vd1329,sK6,vd1303),
inference(unit_resulting_resolution,[],[f1054,f541,f545,f538,f867,f904]) ).
fof(f2113,plain,
vangle(sK4,sK6,sK5) = vangle(sK5,sK6,sK4),
inference(unit_resulting_resolution,[],[f1054,f547,f545,f549,f902,f858]) ).
fof(f2115,plain,
( vangle(sK6,vd1329,sK4) = vangle(sK4,vd1329,sK6)
| spl54_21 ),
inference(unit_resulting_resolution,[],[f1054,f545,f538,f549,f863,f1789]) ).
fof(f2140,plain,
( sF53 = vangle(vd1329,sK4,sK5)
| vd1329 = sK5
| sK4 = sK5
| ~ rpoint(vd1329)
| ~ rpoint(sK4)
| ~ rpoint(sK5) ),
inference(superposition,[],[f1054,f1694]) ).
fof(f2141,plain,
( sF52 = vangle(vd1303,sK5,sK4)
| vd1303 = sK4
| sK4 = sK5
| ~ rpoint(vd1303)
| ~ rpoint(sK5)
| ~ rpoint(sK4) ),
inference(superposition,[],[f1054,f1692]) ).
fof(f2154,plain,
! [X2,X3,X0,X1] :
( vangle(X0,X1,X2) != vd684
| ~ rR(X1,X2,X0)
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| X0 = X1
| X1 = X2
| ~ rline(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(X1)
| X0 = X2
| X1 = X2
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rpoint(X2) ),
inference(superposition,[],[f1124,f1054]) ).
fof(f2159,plain,
! [X2,X3,X0,X1] :
( vangle(X0,X1,X2) != vd684
| ~ rR(X1,X2,X0)
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| X0 = X1
| X1 = X2
| ~ rline(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(X1)
| X0 = X2 ),
inference(duplicate_literal_removal,[],[f2154]) ).
fof(f2175,plain,
( sF52 = vangle(vd1303,sK5,sK4)
| vd1303 = sK4
| ~ rpoint(vd1303)
| ~ rpoint(sK5)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f2141,f858]) ).
fof(f2176,plain,
( sF53 = vangle(vd1329,sK4,sK5)
| vd1329 = sK5
| ~ rpoint(vd1329)
| ~ rpoint(sK4)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f2140,f858]) ).
fof(f2180,plain,
vangle(vd1303,sK6,sK5) = vangle(sK5,sK6,sK4),
inference(forward_demodulation,[],[f2113,f850]) ).
fof(f2181,plain,
( vangle(sK6,vd1303,sK5) = vangle(sK4,vd1329,sK6)
| spl54_21 ),
inference(backward_demodulation,[],[f849,f2115]) ).
fof(f2187,plain,
( sF52 = vangle(vd1303,sK5,sK4)
| vd1303 = sK4
| ~ rpoint(sK5)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f2175,f541]) ).
fof(f2188,plain,
( sF53 = vangle(vd1329,sK4,sK5)
| vd1329 = sK5
| ~ rpoint(sK4)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f2176,f538]) ).
fof(f2197,plain,
( sF52 = vangle(vd1303,sK5,sK4)
| vd1303 = sK4
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f2187,f547]) ).
fof(f2198,plain,
( sF53 = vangle(vd1329,sK4,sK5)
| vd1329 = sK5
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f2188,f549]) ).
fof(f2204,definition,
( spl54_36
<=> vd1303 = sK5 ),
introduced(definition,[new_symbols(definition,[spl54_36])],[avatar_definition]) ).
fof(f2205,plain,
( vd1303 != sK5
| spl54_36 ),
inference(avatar_component_clause,[],[f2204]) ).
fof(f2206,plain,
( vd1303 = sK5
| ~ spl54_36 ),
inference(avatar_component_clause,[],[f2204]) ).
fof(f2208,definition,
( spl54_37
<=> vd1303 = sK4 ),
introduced(definition,[new_symbols(definition,[spl54_37])],[avatar_definition]) ).
fof(f2209,plain,
( vd1303 != sK4
| spl54_37 ),
inference(avatar_component_clause,[],[f2208]) ).
fof(f2210,plain,
( vd1303 = sK4
| ~ spl54_37 ),
inference(avatar_component_clause,[],[f2208]) ).
fof(f2212,definition,
( spl54_38
<=> sF52 = vangle(vd1303,sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl54_38])],[avatar_definition]) ).
fof(f2214,plain,
( sF52 = vangle(vd1303,sK5,sK4)
| ~ spl54_38 ),
inference(avatar_component_clause,[],[f2212]) ).
fof(f2217,definition,
( spl54_39
<=> vd1329 = sK4 ),
introduced(definition,[new_symbols(definition,[spl54_39])],[avatar_definition]) ).
fof(f2218,plain,
( vd1329 != sK4
| spl54_39 ),
inference(avatar_component_clause,[],[f2217]) ).
fof(f2219,plain,
( vd1329 = sK4
| ~ spl54_39 ),
inference(avatar_component_clause,[],[f2217]) ).
fof(f2221,definition,
( spl54_40
<=> vd1329 = sK5 ),
introduced(definition,[new_symbols(definition,[spl54_40])],[avatar_definition]) ).
fof(f2222,plain,
( vd1329 != sK5
| spl54_40 ),
inference(avatar_component_clause,[],[f2221]) ).
fof(f2223,plain,
( vd1329 = sK5
| ~ spl54_40 ),
inference(avatar_component_clause,[],[f2221]) ).
fof(f2225,definition,
( spl54_41
<=> sF53 = vangle(vd1329,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_41])],[avatar_definition]) ).
fof(f2227,plain,
( sF53 = vangle(vd1329,sK4,sK5)
| ~ spl54_41 ),
inference(avatar_component_clause,[],[f2225]) ).
fof(f2229,plain,
( sF52 = vangle(vd1303,sK5,sK4)
| vd1303 = sK4 ),
inference(forward_subsumption_resolution,[],[f2197,f549]) ).
fof(f2230,plain,
( sF53 = vangle(vd1329,sK4,sK5)
| vd1329 = sK5 ),
inference(forward_subsumption_resolution,[],[f2198,f547]) ).
fof(f2235,plain,
( spl54_37
| spl54_38 ),
inference(avatar_split_clause,[],[f2229,f2212,f2208]) ).
fof(f2236,plain,
( spl54_40
| spl54_41 ),
inference(avatar_split_clause,[],[f2230,f2225,f2221]) ).
fof(f2249,plain,
( rR(vd1303,vd1303,sK6)
| ~ spl54_37 ),
inference(backward_demodulation,[],[f1870,f2210]) ).
fof(f2354,plain,
( $false
| ~ spl54_37 ),
inference(forward_subsumption_resolution,[],[f2249,f2020]) ).
fof(f2355,plain,
~ spl54_37,
inference(avatar_contradiction_clause,[],[f2354]) ).
fof(f2386,plain,
( vf(vd1329,vd1329) = vf(vd1303,sK4)
| ~ spl54_40 ),
inference(forward_demodulation,[],[f1982,f2223]) ).
fof(f2409,plain,
( vd684 = vf(vd1303,sK4)
| ~ spl54_40 ),
inference(forward_demodulation,[],[f2386,f1920]) ).
fof(f2530,plain,
! [X0,X1] :
( ~ ron(X0,X1)
| ~ ron(X0,vd1295)
| ~ ron(sK6,X1)
| vd1295 = X1
| ~ rline(X1)
| ~ rline(vd1295)
| sK6 = X0
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(resolution,[],[f1184,f916]) ).
fof(f2598,plain,
( vd684 != vf(vd1303,sK4)
| spl54_37 ),
inference(unit_resulting_resolution,[],[f1080,f541,f549,f2209]) ).
fof(f2610,plain,
( $false
| spl54_37
| ~ spl54_40 ),
inference(forward_subsumption_resolution,[],[f2598,f2409]) ).
fof(f2611,plain,
( spl54_37
| ~ spl54_40 ),
inference(avatar_contradiction_clause,[],[f2610]) ).
fof(f2624,plain,
! [X0] :
( vd684 = sF53
| rR(sK4,sK5,vd1329)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| vd1329 = sK4
| sK4 = sK5
| ~ rline(X0)
| ~ rpoint(vd1329)
| ~ rpoint(sK5)
| ~ rpoint(sK4) ),
inference(superposition,[],[f1694,f1132]) ).
fof(f2750,plain,
( vangle(sK4,sK6,sK5) = vangle(vd1303,sK6,vd1329)
| spl54_21 ),
inference(unit_resulting_resolution,[],[f999,f545,f549,f547,f541,f538,f628,f631,f915,f907,f905,f867,f853,f1789,f863,f621,f852,f902,f909]) ).
fof(f2752,plain,
( vangle(sK5,sK6,sK4) = vangle(vd1329,sK6,vd1303)
| spl54_21 ),
inference(unit_resulting_resolution,[],[f999,f545,f547,f549,f538,f541,f631,f628,f905,f907,f867,f853,f1789,f916,f621,f902,f863,f852,f909]) ).
fof(f2760,plain,
( vangle(sK4,sK6,sK5) = vangle(vd1329,sK6,vd1303)
| spl54_21 ),
inference(forward_demodulation,[],[f2750,f2107]) ).
fof(f2765,plain,
( ! [X0] :
( vd684 = sF53
| rR(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK4,X0)
| sK4 = sK5
| vd1329 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1329)
| ~ rpoint(sK4) )
| ~ spl54_41 ),
inference(superposition,[],[f2227,f1132]) ).
fof(f2773,plain,
( ! [X0] :
( vd684 = sF52
| rR(sK5,vd1303,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK5,X0)
| sK4 = sK5
| vd1303 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1303)
| ~ rpoint(sK5) )
| ~ spl54_38 ),
inference(superposition,[],[f2214,f1132]) ).
fof(f2783,plain,
( vangle(sK5,vd1329,sK4) = vangle(sK4,vd1329,sK5)
| spl54_40 ),
inference(unit_resulting_resolution,[],[f1054,f547,f538,f549,f858,f2222]) ).
fof(f2784,plain,
( vangle(sK5,sK6,vd1329) = vangle(vd1329,sK6,sK5)
| spl54_40 ),
inference(unit_resulting_resolution,[],[f1054,f547,f545,f538,f902,f2222]) ).
fof(f2799,plain,
( vd684 = vangle(vd1329,sK6,sK5)
| spl54_40 ),
inference(forward_demodulation,[],[f2784,f2076]) ).
fof(f2811,plain,
rline(sK7(sK5,sK4)),
inference(unit_resulting_resolution,[],[f1086,f547,f549,f858]) ).
fof(f2874,plain,
! [X0,X1] :
( ~ ron(X0,X1)
| ~ ron(X0,vd1295)
| ~ ron(sK6,X1)
| vd1295 = X1
| ~ rline(X1)
| sK6 = X0
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f2530,f631]) ).
fof(f2886,plain,
( ! [X0] :
( vd684 = sF53
| rR(sK4,sK5,vd1329)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| sK4 = sK5
| ~ rline(X0)
| ~ rpoint(vd1329)
| ~ rpoint(sK5)
| ~ rpoint(sK4) )
| spl54_39 ),
inference(forward_subsumption_resolution,[],[f2624,f2218]) ).
fof(f2903,plain,
( ! [X0] :
( vd684 = sF53
| rR(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK4,X0)
| vd1329 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1329)
| ~ rpoint(sK4) )
| ~ spl54_41 ),
inference(forward_subsumption_resolution,[],[f2765,f858]) ).
fof(f2911,plain,
( ! [X0] :
( vd684 = sF52
| rR(sK5,vd1303,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK5,X0)
| vd1303 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1303)
| ~ rpoint(sK5) )
| ~ spl54_38 ),
inference(forward_subsumption_resolution,[],[f2773,f858]) ).
fof(f2927,plain,
! [X0,X1] :
( ~ ron(sK6,X1)
| ~ ron(X0,vd1295)
| ~ ron(X0,X1)
| vd1295 = X1
| ~ rline(X1)
| sK6 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2874,f545]) ).
fof(f2939,plain,
( ! [X0] :
( vd684 = sF53
| rR(sK4,sK5,vd1329)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(vd1329)
| ~ rpoint(sK5)
| ~ rpoint(sK4) )
| spl54_39 ),
inference(forward_subsumption_resolution,[],[f2886,f858]) ).
fof(f2956,plain,
( ! [X0] :
( vd684 = sF53
| rR(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1329)
| ~ rpoint(sK4) )
| spl54_39
| ~ spl54_41 ),
inference(forward_subsumption_resolution,[],[f2903,f2218]) ).
fof(f2964,plain,
( ! [X0] :
( vd684 = sF52
| rR(sK5,vd1303,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK5,X0)
| vd1303 = sK5
| ~ rline(X0)
| ~ rpoint(vd1303)
| ~ rpoint(sK5) )
| ~ spl54_38 ),
inference(forward_subsumption_resolution,[],[f2911,f549]) ).
fof(f2986,plain,
( ! [X0] :
( vd684 = sF53
| rR(sK4,sK5,vd1329)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4) )
| spl54_39 ),
inference(forward_subsumption_resolution,[],[f2939,f538]) ).
fof(f3002,plain,
( ! [X0] :
( vd684 = sF53
| rR(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(vd1329)
| ~ rpoint(sK4) )
| spl54_39
| ~ spl54_41 ),
inference(forward_subsumption_resolution,[],[f2956,f547]) ).
fof(f3010,plain,
( ! [X0] :
( vd684 = sF52
| rR(sK5,vd1303,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK5,X0)
| vd1303 = sK5
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl54_38 ),
inference(forward_subsumption_resolution,[],[f2964,f541]) ).
fof(f3032,plain,
( ! [X0] :
( vd684 = sF53
| rR(sK4,sK5,vd1329)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK4) )
| spl54_39 ),
inference(forward_subsumption_resolution,[],[f2986,f547]) ).
fof(f3048,plain,
( ! [X0] :
( vd684 = sF53
| rR(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK4) )
| spl54_39
| ~ spl54_41 ),
inference(forward_subsumption_resolution,[],[f3002,f538]) ).
fof(f3056,plain,
( ! [X0] :
( vd684 = sF52
| rR(sK5,vd1303,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK5,X0)
| vd1303 = sK5
| ~ rline(X0) )
| ~ spl54_38 ),
inference(forward_subsumption_resolution,[],[f3010,f547]) ).
fof(f3075,definition,
( spl54_45
<=> rR(sK5,sK4,vd1303) ),
introduced(definition,[new_symbols(definition,[spl54_45])],[avatar_definition]) ).
fof(f3076,plain,
( rR(sK5,sK4,vd1303)
| ~ spl54_45 ),
inference(avatar_component_clause,[],[f3075]) ).
fof(f3077,plain,
( ~ rR(sK5,sK4,vd1303)
| spl54_45 ),
inference(avatar_component_clause,[],[f3075]) ).
fof(f3079,definition,
( spl54_46
<=> vd684 = sF52 ),
introduced(definition,[new_symbols(definition,[spl54_46])],[avatar_definition]) ).
fof(f3080,plain,
( vd684 = sF52
| ~ spl54_46 ),
inference(avatar_component_clause,[],[f3079]) ).
fof(f3085,definition,
( spl54_47
<=> ! [X0] :
( ~ ron(vd1303,X0)
| ~ rline(X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_47])],[avatar_definition]) ).
fof(f3086,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ rline(X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0) )
| ~ spl54_47 ),
inference(avatar_component_clause,[],[f3085]) ).
fof(f3098,plain,
( ! [X0] :
( vd684 = sF53
| rR(sK4,sK5,vd1329)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ rline(X0) )
| spl54_39 ),
inference(forward_subsumption_resolution,[],[f3032,f549]) ).
fof(f3117,plain,
( ! [X0] :
( vd684 = sF53
| rR(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK4,X0)
| ~ rline(X0) )
| spl54_39
| ~ spl54_41 ),
inference(forward_subsumption_resolution,[],[f3048,f549]) ).
fof(f3119,definition,
( spl54_49
<=> rR(sK5,vd1303,sK4) ),
introduced(definition,[new_symbols(definition,[spl54_49])],[avatar_definition]) ).
fof(f3121,plain,
( rR(sK5,vd1303,sK4)
| ~ spl54_49 ),
inference(avatar_component_clause,[],[f3119]) ).
fof(f3124,definition,
( spl54_50
<=> ! [X0] :
( ron(sK4,X0)
| ~ rline(X0)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_50])],[avatar_definition]) ).
fof(f3125,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ rline(X0)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0) )
| ~ spl54_50 ),
inference(avatar_component_clause,[],[f3124]) ).
fof(f3128,definition,
( spl54_51
<=> ! [X0] :
( ~ ron(vd1303,X0)
| ~ rline(X0)
| ~ ron(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_51])],[avatar_definition]) ).
fof(f3129,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ rline(X0)
| ~ ron(vd1303,X0) )
| ~ spl54_51 ),
inference(avatar_component_clause,[],[f3128]) ).
fof(f3141,plain,
( spl54_36
| spl54_47
| spl54_49
| spl54_46
| ~ spl54_38 ),
inference(avatar_split_clause,[],[f3056,f2212,f3079,f3119,f3085,f2204]) ).
fof(f3143,definition,
( spl54_54
<=> rR(sK4,sK5,vd1329) ),
introduced(definition,[new_symbols(definition,[spl54_54])],[avatar_definition]) ).
fof(f3144,plain,
( rR(sK4,sK5,vd1329)
| ~ spl54_54 ),
inference(avatar_component_clause,[],[f3143]) ).
fof(f3145,plain,
( ~ rR(sK4,sK5,vd1329)
| spl54_54 ),
inference(avatar_component_clause,[],[f3143]) ).
fof(f3147,definition,
( spl54_55
<=> vd684 = sF53 ),
introduced(definition,[new_symbols(definition,[spl54_55])],[avatar_definition]) ).
fof(f3148,plain,
( vd684 = sF53
| ~ spl54_55 ),
inference(avatar_component_clause,[],[f3147]) ).
fof(f3152,definition,
( spl54_56
<=> ! [X0] :
( ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ ron(sK4,X0)
| ~ ron(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_56])],[avatar_definition]) ).
fof(f3153,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ rline(X0)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0) )
| ~ spl54_56 ),
inference(avatar_component_clause,[],[f3152]) ).
fof(f3162,plain,
( spl54_56
| spl54_54
| spl54_55
| spl54_39 ),
inference(avatar_split_clause,[],[f3098,f2217,f3147,f3143,f3152]) ).
fof(f3164,definition,
( spl54_58
<=> rR(sK4,vd1329,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_58])],[avatar_definition]) ).
fof(f3166,plain,
( rR(sK4,vd1329,sK5)
| ~ spl54_58 ),
inference(avatar_component_clause,[],[f3164]) ).
fof(f3169,definition,
( spl54_59
<=> ! [X0] :
( ron(sK5,X0)
| ~ rline(X0)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_59])],[avatar_definition]) ).
fof(f3170,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ rline(X0)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0) )
| ~ spl54_59 ),
inference(avatar_component_clause,[],[f3169]) ).
fof(f3173,definition,
( spl54_60
<=> ! [X0] :
( ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ ron(sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_60])],[avatar_definition]) ).
fof(f3174,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ rline(X0)
| ~ ron(vd1329,X0) )
| ~ spl54_60 ),
inference(avatar_component_clause,[],[f3173]) ).
fof(f3176,plain,
( spl54_56
| spl54_58
| spl54_55
| spl54_39
| ~ spl54_41 ),
inference(avatar_split_clause,[],[f3117,f2225,f2217,f3147,f3164,f3152]) ).
fof(f3185,plain,
( sF52 = vangle(sK4,vd1303,vd1303)
| ~ spl54_36 ),
inference(backward_demodulation,[],[f1692,f2206]) ).
fof(f3186,plain,
( sF53 = vangle(vd1303,sK4,vd1329)
| ~ spl54_36 ),
inference(backward_demodulation,[],[f1694,f2206]) ).
fof(f3315,plain,
( vangle(sK5,vd1329,vd1329) = vangle(vd1329,vd1303,sK5)
| ~ spl54_39 ),
inference(forward_demodulation,[],[f845,f2219]) ).
fof(f3346,plain,
( sF53 = vangle(vd1303,vd1329,vd1329)
| ~ spl54_36
| ~ spl54_39 ),
inference(forward_demodulation,[],[f3186,f2219]) ).
fof(f3347,plain,
( sF52 = vangle(vd1329,vd1303,vd1303)
| ~ spl54_36
| ~ spl54_39 ),
inference(forward_demodulation,[],[f3185,f2219]) ).
fof(f3358,plain,
( vangle(vd1303,vd1329,vd1329) = vangle(vd1329,vd1303,vd1303)
| ~ spl54_36
| ~ spl54_39 ),
inference(forward_demodulation,[],[f3315,f2206]) ).
fof(f3373,plain,
( sF52 = vangle(vd1303,vd1329,vd1329)
| ~ spl54_36
| ~ spl54_39 ),
inference(forward_demodulation,[],[f3358,f3347]) ).
fof(f3379,plain,
( sF52 = sF53
| ~ spl54_36
| ~ spl54_39 ),
inference(backward_demodulation,[],[f3346,f3373]) ).
fof(f3380,plain,
( $false
| ~ spl54_36
| ~ spl54_39 ),
inference(forward_subsumption_resolution,[],[f3379,f1695]) ).
fof(f3381,plain,
( ~ spl54_36
| ~ spl54_39 ),
inference(avatar_contradiction_clause,[],[f3380]) ).
fof(f3388,plain,
( vf(vd1303,sK5) = vf(vd1329,vd1329)
| ~ spl54_39 ),
inference(forward_demodulation,[],[f848,f2219]) ).
fof(f3428,plain,
( vd684 = vf(vd1303,sK5)
| ~ spl54_39 ),
inference(forward_demodulation,[],[f3388,f1920]) ).
fof(f3573,plain,
( vd684 != vf(vd1303,sK5)
| spl54_36 ),
inference(unit_resulting_resolution,[],[f1080,f541,f547,f2205]) ).
fof(f3585,plain,
( $false
| spl54_36
| ~ spl54_39 ),
inference(forward_subsumption_resolution,[],[f3573,f3428]) ).
fof(f3586,plain,
( spl54_36
| ~ spl54_39 ),
inference(avatar_contradiction_clause,[],[f3585]) ).
fof(f3601,plain,
( vangle(vd1303,sK6,sK5) = vangle(vd1329,sK6,vd1303)
| spl54_21 ),
inference(backward_demodulation,[],[f2180,f2752]) ).
fof(f3603,plain,
( vangle(sK4,vd1303,sK5) = vangle(sK4,vd1329,sK5)
| spl54_40 ),
inference(backward_demodulation,[],[f845,f2783]) ).
fof(f3632,plain,
( vangle(sK4,sK6,vd1329) = vangle(vd1329,sK6,vd1303)
| spl54_21 ),
inference(backward_demodulation,[],[f1865,f3601]) ).
fof(f3885,plain,
( vangle(sK4,sK6,vd1329) = vangle(vd1329,sK6,sK4)
| spl54_21
| spl54_39 ),
inference(unit_resulting_resolution,[],[f1054,f549,f545,f538,f1789,f2218]) ).
fof(f3897,plain,
( vd684 != vf(vd1329,sK4)
| spl54_39 ),
inference(unit_resulting_resolution,[],[f1080,f538,f549,f2218]) ).
fof(f3899,plain,
( vangle(vd1329,sK6,vd1303) = vangle(vd1329,sK6,sK4)
| spl54_21
| spl54_39 ),
inference(forward_demodulation,[],[f3885,f3632]) ).
fof(f3936,plain,
( ~ ron(sK5,vd1297)
| ~ spl54_47 ),
inference(unit_resulting_resolution,[],[f3086,f628,f907,f905]) ).
fof(f3940,definition,
( spl54_61
<=> ron(sK4,vd1295) ),
introduced(definition,[new_symbols(definition,[spl54_61])],[avatar_definition]) ).
fof(f3941,plain,
( ron(sK4,vd1295)
| ~ spl54_61 ),
inference(avatar_component_clause,[],[f3940]) ).
fof(f3942,plain,
( ~ ron(sK4,vd1295)
| spl54_61 ),
inference(avatar_component_clause,[],[f3940]) ).
fof(f3948,plain,
( ~ ron(sK4,vd1295)
| ~ spl54_56 ),
inference(unit_resulting_resolution,[],[f3153,f631,f621,f909]) ).
fof(f3960,plain,
! [X0] :
( ~ ron(X0,vd1295)
| ~ ron(X0,vd1297)
| vd1295 = vd1297
| ~ rline(vd1297)
| sK6 = X0
| ~ rpoint(X0) ),
inference(resolution,[],[f2927,f915]) ).
fof(f3962,plain,
! [X0] :
( ~ ron(X0,vd1295)
| ~ ron(X0,vd1297)
| vd1295 = vd1297
| sK6 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f3960,f628]) ).
fof(f3964,definition,
( spl54_63
<=> vd1295 = vd1297 ),
introduced(definition,[new_symbols(definition,[spl54_63])],[avatar_definition]) ).
fof(f3966,plain,
( vd1295 = vd1297
| ~ spl54_63 ),
inference(avatar_component_clause,[],[f3964]) ).
fof(f3968,definition,
( spl54_64
<=> ! [X0] :
( ~ ron(X0,vd1295)
| ~ rpoint(X0)
| sK6 = X0
| ~ ron(X0,vd1297) ) ),
introduced(definition,[new_symbols(definition,[spl54_64])],[avatar_definition]) ).
fof(f3969,plain,
( ! [X0] :
( ~ ron(X0,vd1297)
| ~ rpoint(X0)
| sK6 = X0
| ~ ron(X0,vd1295) )
| ~ spl54_64 ),
inference(avatar_component_clause,[],[f3968]) ).
fof(f3970,plain,
( spl54_63
| spl54_64 ),
inference(avatar_split_clause,[],[f3962,f3968,f3964]) ).
fof(f3973,plain,
( ron(sK4,vd1295)
| ~ spl54_63 ),
inference(backward_demodulation,[],[f907,f3966]) ).
fof(f3978,plain,
( ~ ron(sK5,vd1295)
| ~ spl54_47
| ~ spl54_63 ),
inference(backward_demodulation,[],[f3936,f3966]) ).
fof(f3979,plain,
( $false
| ~ spl54_47
| ~ spl54_63 ),
inference(forward_subsumption_resolution,[],[f3978,f909]) ).
fof(f3980,plain,
( ~ spl54_47
| ~ spl54_63 ),
inference(avatar_contradiction_clause,[],[f3979]) ).
fof(f3984,plain,
( $false
| spl54_61
| ~ spl54_63 ),
inference(forward_subsumption_resolution,[],[f3973,f3942]) ).
fof(f3985,plain,
( spl54_61
| ~ spl54_63 ),
inference(avatar_contradiction_clause,[],[f3984]) ).
fof(f3993,plain,
( ~ rR(sK5,sK4,vd1329)
| ~ spl54_54 ),
inference(unit_resulting_resolution,[],[f1018,f549,f547,f538,f3144]) ).
fof(f3995,plain,
( rR(sK4,vd1329,sK5)
| ~ spl54_54 ),
inference(unit_resulting_resolution,[],[f1029,f547,f549,f538,f3144]) ).
fof(f4008,plain,
( ~ rR(sK4,sK5,vd1303)
| ~ spl54_45 ),
inference(unit_resulting_resolution,[],[f1018,f547,f549,f541,f3076]) ).
fof(f4010,plain,
( rR(sK5,vd1303,sK4)
| ~ spl54_45 ),
inference(unit_resulting_resolution,[],[f1029,f549,f547,f541,f3076]) ).
fof(f4023,plain,
( rR(sK4,vd1329,vd1303)
| ~ spl54_45
| ~ spl54_58 ),
inference(unit_resulting_resolution,[],[f1015,f538,f549,f547,f541,f3076,f3166]) ).
fof(f4024,plain,
( ~ rR(vd1329,sK4,sK5)
| ~ spl54_58 ),
inference(unit_resulting_resolution,[],[f1018,f549,f538,f547,f3166]) ).
fof(f4062,plain,
( ~ rR(vd1303,sK5,sK4)
| ~ spl54_49 ),
inference(unit_resulting_resolution,[],[f1018,f547,f541,f549,f3121]) ).
fof(f4065,plain,
( rR(sK5,vd1303,sK6)
| ~ spl54_49 ),
inference(unit_resulting_resolution,[],[f1214,f541,f549,f545,f547,f1870,f3121]) ).
fof(f4082,plain,
! [X0] :
( vd684 = vangle(vd1329,sK5,sK4)
| rR(sK4,vd1303,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| sK4 = sK5
| vd1303 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| ~ rpoint(sK4) ),
inference(superposition,[],[f843,f1132]) ).
fof(f4087,plain,
! [X0] :
( vd684 != vangle(vd1329,sK5,sK4)
| ~ rR(sK4,vd1303,sK5)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| sK4 = sK5
| vd1303 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| ~ rpoint(sK4) ),
inference(superposition,[],[f1124,f843]) ).
fof(f4088,plain,
! [X0] :
( vd684 != vangle(vd1329,sK5,sK4)
| ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| sK4 = sK5
| vd1303 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| ~ rpoint(sK4) ),
inference(superposition,[],[f1128,f843]) ).
fof(f4091,plain,
! [X0] :
( vd684 != vangle(vd1329,sK5,sK4)
| ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| vd1303 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f4088,f858]) ).
fof(f4092,plain,
! [X0] :
( vd684 != vangle(vd1329,sK5,sK4)
| ~ rR(sK4,vd1303,sK5)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| vd1303 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f4087,f858]) ).
fof(f4097,plain,
! [X0] :
( vd684 = vangle(vd1329,sK5,sK4)
| rR(sK4,vd1303,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| vd1303 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| ~ rpoint(sK4) ),
inference(forward_subsumption_resolution,[],[f4082,f858]) ).
fof(f4099,plain,
( ! [X0] :
( vd684 != vangle(vd1329,sK5,sK4)
| ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| ~ rpoint(sK4) )
| spl54_37 ),
inference(forward_subsumption_resolution,[],[f4091,f2209]) ).
fof(f4100,plain,
( ! [X0] :
( vd684 != vangle(vd1329,sK5,sK4)
| ~ rR(sK4,vd1303,sK5)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| ~ rpoint(sK4) )
| spl54_37 ),
inference(forward_subsumption_resolution,[],[f4092,f2209]) ).
fof(f4105,plain,
( ! [X0] :
( vd684 = vangle(vd1329,sK5,sK4)
| rR(sK4,vd1303,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| ~ rpoint(sK4) )
| spl54_37 ),
inference(forward_subsumption_resolution,[],[f4097,f2209]) ).
fof(f4107,plain,
( ! [X0] :
( vd684 != vangle(vd1329,sK5,sK4)
| ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(vd1303)
| ~ rpoint(sK4) )
| spl54_37 ),
inference(forward_subsumption_resolution,[],[f4099,f547]) ).
fof(f4108,plain,
( ! [X0] :
( vd684 != vangle(vd1329,sK5,sK4)
| ~ rR(sK4,vd1303,sK5)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(vd1303)
| ~ rpoint(sK4) )
| spl54_37 ),
inference(forward_subsumption_resolution,[],[f4100,f547]) ).
fof(f4113,plain,
( ! [X0] :
( vd684 = vangle(vd1329,sK5,sK4)
| rR(sK4,vd1303,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(vd1303)
| ~ rpoint(sK4) )
| spl54_37 ),
inference(forward_subsumption_resolution,[],[f4105,f547]) ).
fof(f4115,plain,
( ! [X0] :
( vd684 != vangle(vd1329,sK5,sK4)
| ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK4) )
| spl54_37 ),
inference(forward_subsumption_resolution,[],[f4107,f541]) ).
fof(f4116,plain,
( ! [X0] :
( vd684 != vangle(vd1329,sK5,sK4)
| ~ rR(sK4,vd1303,sK5)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK4) )
| spl54_37 ),
inference(forward_subsumption_resolution,[],[f4108,f541]) ).
fof(f4121,plain,
( ! [X0] :
( vd684 = vangle(vd1329,sK5,sK4)
| rR(sK4,vd1303,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK4) )
| spl54_37 ),
inference(forward_subsumption_resolution,[],[f4113,f541]) ).
fof(f4123,plain,
( ! [X0] :
( vd684 != vangle(vd1329,sK5,sK4)
| ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0) )
| spl54_37 ),
inference(forward_subsumption_resolution,[],[f4115,f549]) ).
fof(f4124,plain,
( ! [X0] :
( vd684 != vangle(vd1329,sK5,sK4)
| ~ rR(sK4,vd1303,sK5)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0) )
| spl54_37 ),
inference(forward_subsumption_resolution,[],[f4116,f549]) ).
fof(f4129,plain,
( ! [X0] :
( vd684 = vangle(vd1329,sK5,sK4)
| rR(sK4,vd1303,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0) )
| spl54_37 ),
inference(forward_subsumption_resolution,[],[f4121,f549]) ).
fof(f4131,definition,
( spl54_65
<=> rR(sK4,vd1303,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_65])],[avatar_definition]) ).
fof(f4132,plain,
( ~ rR(sK4,vd1303,sK5)
| spl54_65 ),
inference(avatar_component_clause,[],[f4131]) ).
fof(f4133,plain,
( rR(sK4,vd1303,sK5)
| ~ spl54_65 ),
inference(avatar_component_clause,[],[f4131]) ).
fof(f4135,definition,
( spl54_66
<=> vd684 = vangle(vd1329,sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl54_66])],[avatar_definition]) ).
fof(f4136,plain,
( vd684 != vangle(vd1329,sK5,sK4)
| spl54_66 ),
inference(avatar_component_clause,[],[f4135]) ).
fof(f4137,plain,
( vd684 = vangle(vd1329,sK5,sK4)
| ~ spl54_66 ),
inference(avatar_component_clause,[],[f4135]) ).
fof(f4140,definition,
( spl54_67
<=> ! [X0] :
( ron(sK5,X0)
| ~ rline(X0)
| ~ ron(sK4,X0)
| ~ ron(vd1303,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_67])],[avatar_definition]) ).
fof(f4141,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ rline(X0)
| ron(sK5,X0)
| ~ ron(vd1303,X0) )
| ~ spl54_67 ),
inference(avatar_component_clause,[],[f4140]) ).
fof(f4142,plain,
( spl54_67
| ~ spl54_66
| spl54_37 ),
inference(avatar_split_clause,[],[f4123,f2208,f4135,f4140]) ).
fof(f4144,definition,
( spl54_68
<=> ! [X0] :
( ~ ron(vd1303,X0)
| ~ rline(X0)
| ~ ron(sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_68])],[avatar_definition]) ).
fof(f4145,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ rline(X0)
| ~ ron(vd1303,X0) )
| ~ spl54_68 ),
inference(avatar_component_clause,[],[f4144]) ).
fof(f4146,plain,
( spl54_68
| ~ spl54_65
| ~ spl54_66
| spl54_37 ),
inference(avatar_split_clause,[],[f4124,f2208,f4135,f4131,f4144]) ).
fof(f4147,plain,
( spl54_47
| spl54_65
| spl54_66
| spl54_37 ),
inference(avatar_split_clause,[],[f4129,f2208,f4135,f4131,f3085]) ).
fof(f4158,plain,
( vd1295 = vd1297
| spl54_21
| ~ spl54_61 ),
inference(unit_resulting_resolution,[],[f1184,f549,f545,f631,f628,f1789,f907,f3941,f916,f915]) ).
fof(f4192,plain,
( ~ ron(sK5,vd1297)
| ~ spl54_64 ),
inference(unit_resulting_resolution,[],[f3969,f547,f909,f902]) ).
fof(f4201,plain,
( ! [X0] :
( vd684 != vd684
| rR(sK5,vd1329,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| sK4 = sK5
| vd1329 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_66 ),
inference(superposition,[],[f4136,f1132]) ).
fof(f4204,plain,
( ! [X0] :
( rR(sK5,vd1329,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| sK4 = sK5
| vd1329 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_66 ),
inference(trivial_inequality_removal,[],[f4201]) ).
fof(f4207,plain,
( ! [X0] :
( rR(sK5,vd1329,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| vd1329 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_66 ),
inference(forward_subsumption_resolution,[],[f4204,f858]) ).
fof(f4210,plain,
( ! [X0] :
( rR(sK5,vd1329,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_40
| spl54_66 ),
inference(forward_subsumption_resolution,[],[f4207,f2222]) ).
fof(f4213,plain,
( ! [X0] :
( rR(sK5,vd1329,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_40
| spl54_66 ),
inference(forward_subsumption_resolution,[],[f4210,f549]) ).
fof(f4216,plain,
( ! [X0] :
( rR(sK5,vd1329,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| spl54_40
| spl54_66 ),
inference(forward_subsumption_resolution,[],[f4213,f538]) ).
fof(f4219,plain,
( ! [X0] :
( rR(sK5,vd1329,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0) )
| spl54_40
| spl54_66 ),
inference(forward_subsumption_resolution,[],[f4216,f547]) ).
fof(f4221,definition,
( spl54_69
<=> rR(sK5,vd1329,sK4) ),
introduced(definition,[new_symbols(definition,[spl54_69])],[avatar_definition]) ).
fof(f4222,plain,
( ~ rR(sK5,vd1329,sK4)
| spl54_69 ),
inference(avatar_component_clause,[],[f4221]) ).
fof(f4223,plain,
( rR(sK5,vd1329,sK4)
| ~ spl54_69 ),
inference(avatar_component_clause,[],[f4221]) ).
fof(f4224,plain,
( spl54_56
| spl54_69
| spl54_40
| spl54_66 ),
inference(avatar_split_clause,[],[f4219,f4135,f2221,f4221,f3152]) ).
fof(f4321,plain,
ron(sK4,sK7(sK5,sK4)),
inference(unit_resulting_resolution,[],[f1082,f547,f549,f858]) ).
fof(f4364,plain,
ron(sK5,sK7(sK5,sK4)),
inference(unit_resulting_resolution,[],[f1084,f547,f549,f858]) ).
fof(f4468,plain,
( spl54_63
| spl54_21
| ~ spl54_61 ),
inference(avatar_split_clause,[],[f4158,f3940,f1787,f3964]) ).
fof(f4530,plain,
( ! [X0] :
( vd684 != vd684
| ~ rR(sK5,vd1329,sK4)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| sK4 = sK5
| vd1329 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| ~ spl54_66 ),
inference(superposition,[],[f1124,f4137]) ).
fof(f4531,plain,
( ! [X0] :
( vd684 != vd684
| ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| sK4 = sK5
| vd1329 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| ~ spl54_66 ),
inference(superposition,[],[f1128,f4137]) ).
fof(f4532,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| sK4 = sK5
| vd1329 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| ~ spl54_66 ),
inference(trivial_inequality_removal,[],[f4531]) ).
fof(f4533,plain,
( ! [X0] :
( ~ rR(sK5,vd1329,sK4)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| sK4 = sK5
| vd1329 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| ~ spl54_66 ),
inference(trivial_inequality_removal,[],[f4530]) ).
fof(f4534,plain,
( ! [X0] :
( ~ rR(sK5,vd1329,sK4)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| vd1329 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| ~ spl54_66 ),
inference(forward_subsumption_resolution,[],[f4533,f858]) ).
fof(f4540,plain,
( ! [X0] :
( ~ rR(sK5,vd1329,sK4)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_40
| ~ spl54_66 ),
inference(forward_subsumption_resolution,[],[f4534,f2222]) ).
fof(f4545,plain,
( ! [X0] :
( ~ rR(sK5,vd1329,sK4)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_40
| ~ spl54_66 ),
inference(forward_subsumption_resolution,[],[f4540,f549]) ).
fof(f4550,plain,
( ! [X0] :
( ~ rR(sK5,vd1329,sK4)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| spl54_40
| ~ spl54_66 ),
inference(forward_subsumption_resolution,[],[f4545,f538]) ).
fof(f4555,plain,
( ! [X0] :
( ~ rR(sK5,vd1329,sK4)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0) )
| spl54_40
| ~ spl54_66 ),
inference(forward_subsumption_resolution,[],[f4550,f547]) ).
fof(f4561,definition,
( spl54_70
<=> ! [X0] :
( ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ ron(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_70])],[avatar_definition]) ).
fof(f4562,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ rline(X0)
| ~ ron(vd1329,X0) )
| ~ spl54_70 ),
inference(avatar_component_clause,[],[f4561]) ).
fof(f4563,plain,
( spl54_70
| ~ spl54_69
| spl54_40
| ~ spl54_66 ),
inference(avatar_split_clause,[],[f4555,f4135,f2221,f4221,f4561]) ).
fof(f4571,plain,
( ~ rR(sK6,sK4,sK5)
| spl54_65 ),
inference(unit_resulting_resolution,[],[f1015,f541,f549,f545,f547,f1870,f4132]) ).
fof(f4573,plain,
( ~ rR(sK4,sK5,vd1303)
| spl54_65 ),
inference(unit_resulting_resolution,[],[f1029,f547,f549,f541,f4132]) ).
fof(f4667,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| ~ spl54_58 ),
inference(resolution,[],[f1178,f3166]) ).
fof(f4671,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(vd1303) )
| ~ spl54_49 ),
inference(resolution,[],[f1178,f3121]) ).
fof(f4682,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1303) )
| ~ spl54_49 ),
inference(forward_subsumption_resolution,[],[f4671,f549]) ).
fof(f4686,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| ~ spl54_58 ),
inference(forward_subsumption_resolution,[],[f4667,f547]) ).
fof(f4692,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(vd1303) )
| ~ spl54_49 ),
inference(forward_subsumption_resolution,[],[f4682,f547]) ).
fof(f4696,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(vd1329) )
| ~ spl54_58 ),
inference(forward_subsumption_resolution,[],[f4686,f549]) ).
fof(f4702,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ron(sK4,X0)
| ~ rline(X0) )
| ~ spl54_49 ),
inference(forward_subsumption_resolution,[],[f4692,f541]) ).
fof(f4706,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ron(sK5,X0)
| ~ rline(X0) )
| ~ spl54_58 ),
inference(forward_subsumption_resolution,[],[f4696,f538]) ).
fof(f4709,plain,
( spl54_50
| ~ spl54_49 ),
inference(avatar_split_clause,[],[f4702,f3119,f3124]) ).
fof(f4710,plain,
( spl54_59
| ~ spl54_58 ),
inference(avatar_split_clause,[],[f4706,f3164,f3169]) ).
fof(f4712,plain,
( vd684 != sF53
| ~ spl54_46 ),
inference(backward_demodulation,[],[f1695,f3080]) ).
fof(f4774,plain,
( ~ rR(sK5,vd1303,sK4)
| spl54_45 ),
inference(unit_resulting_resolution,[],[f1029,f541,f547,f549,f3077]) ).
fof(f4860,plain,
( ! [X0] :
( rR(sK4,sK5,vd1303)
| rR(vd1303,sK5,sK4)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| vd1303 = sK4
| vd1303 = sK5
| sK4 = sK5
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK5) )
| spl54_45 ),
inference(resolution,[],[f1174,f3077]) ).
fof(f4861,plain,
! [X0] :
( rR(sK5,sK6,vd1329)
| rR(vd1329,sK6,sK5)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| vd1329 = sK5
| vd1329 = sK6
| sK5 = sK6
| ~ rpoint(vd1329)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(resolution,[],[f1174,f852]) ).
fof(f4879,plain,
( ! [X0] :
( rR(sK5,sK6,vd1329)
| rR(vd1329,sK6,sK5)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| vd1329 = sK6
| sK5 = sK6
| ~ rpoint(vd1329)
| ~ rpoint(sK5)
| ~ rpoint(sK6) )
| spl54_40 ),
inference(forward_subsumption_resolution,[],[f4861,f2222]) ).
fof(f4880,plain,
( ! [X0] :
( rR(sK4,sK5,vd1303)
| rR(vd1303,sK5,sK4)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| vd1303 = sK4
| vd1303 = sK5
| sK4 = sK5
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK5) )
| spl54_45
| ~ spl54_67 ),
inference(forward_subsumption_resolution,[],[f4860,f4141]) ).
fof(f4885,plain,
( ! [X0] :
( rR(sK5,sK6,vd1329)
| rR(vd1329,sK6,sK5)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| sK5 = sK6
| ~ rpoint(vd1329)
| ~ rpoint(sK5)
| ~ rpoint(sK6) )
| spl54_40 ),
inference(forward_subsumption_resolution,[],[f4879,f863]) ).
fof(f4886,plain,
( ! [X0] :
( rR(vd1303,sK5,sK4)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| vd1303 = sK4
| vd1303 = sK5
| sK4 = sK5
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK5) )
| spl54_45
| spl54_65
| ~ spl54_67 ),
inference(forward_subsumption_resolution,[],[f4880,f4573]) ).
fof(f4890,plain,
( ! [X0] :
( rR(sK5,sK6,vd1329)
| rR(vd1329,sK6,sK5)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(vd1329)
| ~ rpoint(sK5)
| ~ rpoint(sK6) )
| spl54_40 ),
inference(forward_subsumption_resolution,[],[f4885,f902]) ).
fof(f4891,plain,
( ! [X0] :
( rR(vd1303,sK5,sK4)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| vd1303 = sK5
| sK4 = sK5
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK5) )
| spl54_37
| spl54_45
| spl54_65
| ~ spl54_67 ),
inference(forward_subsumption_resolution,[],[f4886,f2209]) ).
fof(f4902,plain,
( ! [X0] :
( rR(sK5,sK6,vd1329)
| rR(vd1329,sK6,sK5)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6) )
| spl54_40 ),
inference(forward_subsumption_resolution,[],[f4890,f538]) ).
fof(f4903,plain,
( ! [X0] :
( rR(vd1303,sK5,sK4)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| sK4 = sK5
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK5) )
| spl54_36
| spl54_37
| spl54_45
| spl54_65
| ~ spl54_67 ),
inference(forward_subsumption_resolution,[],[f4891,f2205]) ).
fof(f4904,plain,
( ! [X0] :
( rR(sK5,sK6,vd1329)
| rR(vd1329,sK6,sK5)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK6) )
| spl54_40 ),
inference(forward_subsumption_resolution,[],[f4902,f547]) ).
fof(f4905,plain,
( ! [X0] :
( rR(vd1303,sK5,sK4)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK5) )
| spl54_36
| spl54_37
| spl54_45
| spl54_65
| ~ spl54_67 ),
inference(forward_subsumption_resolution,[],[f4903,f858]) ).
fof(f4906,plain,
( ! [X0] :
( rR(sK5,sK6,vd1329)
| rR(vd1329,sK6,sK5)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0) )
| spl54_40 ),
inference(forward_subsumption_resolution,[],[f4904,f545]) ).
fof(f4907,plain,
( ! [X0] :
( rR(vd1303,sK5,sK4)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5) )
| spl54_36
| spl54_37
| spl54_45
| spl54_65
| ~ spl54_67 ),
inference(forward_subsumption_resolution,[],[f4905,f541]) ).
fof(f4909,definition,
( spl54_73
<=> ! [X0] :
( ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_73])],[avatar_definition]) ).
fof(f4910,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0) )
| ~ spl54_73 ),
inference(avatar_component_clause,[],[f4909]) ).
fof(f4912,definition,
( spl54_74
<=> rR(vd1329,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_74])],[avatar_definition]) ).
fof(f4914,plain,
( rR(vd1329,sK6,sK5)
| ~ spl54_74 ),
inference(avatar_component_clause,[],[f4912]) ).
fof(f4916,definition,
( spl54_75
<=> rR(sK5,sK6,vd1329) ),
introduced(definition,[new_symbols(definition,[spl54_75])],[avatar_definition]) ).
fof(f4918,plain,
( rR(sK5,sK6,vd1329)
| ~ spl54_75 ),
inference(avatar_component_clause,[],[f4916]) ).
fof(f4919,plain,
( spl54_73
| spl54_74
| spl54_75
| spl54_40 ),
inference(avatar_split_clause,[],[f4906,f2221,f4916,f4912,f4909]) ).
fof(f4920,plain,
( ! [X0] :
( rR(vd1303,sK5,sK4)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| spl54_36
| spl54_37
| spl54_45
| spl54_65
| ~ spl54_67 ),
inference(forward_subsumption_resolution,[],[f4907,f549]) ).
fof(f4921,plain,
( ! [X0] :
( rR(vd1303,sK5,sK4)
| ~ ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ rline(X0) )
| spl54_36
| spl54_37
| spl54_45
| spl54_65
| ~ spl54_67 ),
inference(forward_subsumption_resolution,[],[f4920,f547]) ).
fof(f4923,definition,
( spl54_76
<=> rR(vd1303,sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl54_76])],[avatar_definition]) ).
fof(f4924,plain,
( ~ rR(vd1303,sK5,sK4)
| spl54_76 ),
inference(avatar_component_clause,[],[f4923]) ).
fof(f4925,plain,
( rR(vd1303,sK5,sK4)
| ~ spl54_76 ),
inference(avatar_component_clause,[],[f4923]) ).
fof(f4926,plain,
( spl54_68
| spl54_76
| spl54_36
| spl54_37
| spl54_45
| spl54_65
| ~ spl54_67 ),
inference(avatar_split_clause,[],[f4921,f4140,f4131,f3075,f2208,f2204,f4923,f4144]) ).
fof(f5446,plain,
( ! [X0] :
( rR(vd1329,sK5,sK4)
| rR(sK4,sK5,vd1329)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| vd1329 = sK4
| sK4 = sK5
| vd1329 = sK5
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_69 ),
inference(resolution,[],[f4222,f1174]) ).
fof(f5463,plain,
( ~ rline(vd1295)
| ~ ron(vd1329,vd1295)
| ~ ron(sK5,vd1295)
| ~ spl54_73 ),
inference(resolution,[],[f4910,f916]) ).
fof(f5469,plain,
( ~ ron(vd1329,vd1295)
| ~ ron(sK5,vd1295)
| ~ spl54_73 ),
inference(forward_subsumption_resolution,[],[f5463,f631]) ).
fof(f5480,plain,
( ~ ron(sK5,vd1295)
| ~ spl54_73 ),
inference(forward_subsumption_resolution,[],[f5469,f621]) ).
fof(f5481,plain,
( $false
| ~ spl54_73 ),
inference(forward_subsumption_resolution,[],[f5480,f909]) ).
fof(f5482,plain,
~ spl54_73,
inference(avatar_contradiction_clause,[],[f5481]) ).
fof(f5486,plain,
( rR(sK5,vd1329,sK6)
| ~ spl54_75 ),
inference(unit_resulting_resolution,[],[f1029,f545,f547,f538,f4918]) ).
fof(f7090,plain,
( rR(sK4,vd1329,sK6)
| ~ spl54_58
| ~ spl54_75 ),
inference(unit_resulting_resolution,[],[f1214,f538,f547,f545,f549,f3166,f5486]) ).
fof(f7129,plain,
( ~ rR(sK4,vd1329,vd1303)
| ~ spl54_58
| ~ spl54_75 ),
inference(unit_resulting_resolution,[],[f1372,f538,f549,f545,f541,f855,f7090]) ).
fof(f7171,plain,
( rR(vd1329,sK5,sK6)
| ~ spl54_74 ),
inference(unit_resulting_resolution,[],[f1029,f545,f538,f547,f4914]) ).
fof(f7249,plain,
( rR(sK4,sK5,sK6)
| ~ spl54_54
| ~ spl54_74 ),
inference(unit_resulting_resolution,[],[f1214,f547,f538,f545,f549,f3144,f7171]) ).
fof(f7296,plain,
( ~ rR(sK4,vd1329,sK6)
| ~ spl54_54
| ~ spl54_74 ),
inference(unit_resulting_resolution,[],[f1372,f547,f549,f538,f545,f3144,f7249]) ).
fof(f7378,plain,
( ! [X0] :
( vd684 = vangle(sK4,vd1329,sK5)
| rR(vd1303,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK5
| vd1303 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) )
| spl54_40 ),
inference(superposition,[],[f3603,f1132]) ).
fof(f7386,plain,
( ! [X0] :
( vd684 != vangle(sK4,vd1329,sK5)
| ~ rR(vd1303,sK5,sK4)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK4
| vd1303 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| sK4 = sK5 )
| spl54_40 ),
inference(superposition,[],[f2159,f3603]) ).
fof(f7693,plain,
( ! [X0] :
( vd684 = vangle(sK4,vd1329,sK6)
| rR(vd1303,sK6,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK5
| vd1303 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(vd1303) )
| spl54_21 ),
inference(superposition,[],[f1132,f2181]) ).
fof(f7895,plain,
( vd684 = vangle(sK4,sK6,sK5)
| spl54_21
| ~ spl54_61
| spl54_65 ),
inference(unit_resulting_resolution,[],[f1132,f545,f549,f547,f631,f3941,f909,f916,f1789,f902,f4571]) ).
fof(f7904,plain,
( vd684 = vangle(vd1329,sK6,vd1303)
| spl54_21
| ~ spl54_61
| spl54_65 ),
inference(backward_demodulation,[],[f2760,f7895]) ).
fof(f7913,plain,
( vd684 = vangle(sK4,sK6,vd1329)
| spl54_21
| ~ spl54_61
| spl54_65 ),
inference(backward_demodulation,[],[f3632,f7904]) ).
fof(f7975,plain,
( ~ rR(sK6,vd1329,sK4)
| spl54_21
| spl54_39
| ~ spl54_61
| spl54_65 ),
inference(unit_resulting_resolution,[],[f2159,f631,f545,f538,f549,f621,f916,f2218,f863,f1789,f7913]) ).
fof(f8418,plain,
( ! [X0] :
( vd684 != vangle(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK4
| vd1303 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| sK4 = sK5 )
| spl54_40
| ~ spl54_76 ),
inference(forward_subsumption_resolution,[],[f7386,f4925]) ).
fof(f8452,plain,
( $false
| ~ spl54_46
| ~ spl54_55 ),
inference(forward_subsumption_resolution,[],[f4712,f3148]) ).
fof(f8453,plain,
( ~ spl54_46
| ~ spl54_55 ),
inference(avatar_contradiction_clause,[],[f8452]) ).
fof(f8460,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| vd1329 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| ~ spl54_66 ),
inference(forward_subsumption_resolution,[],[f4532,f858]) ).
fof(f8463,plain,
( ! [X0] :
( rR(vd1329,sK5,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| vd1329 = sK4
| sK4 = sK5
| vd1329 = sK5
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_54
| spl54_69 ),
inference(forward_subsumption_resolution,[],[f5446,f3145]) ).
fof(f8464,plain,
( ! [X0] :
( vd684 != vangle(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK5
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| sK4 = sK5 )
| spl54_37
| spl54_40
| ~ spl54_76 ),
inference(forward_subsumption_resolution,[],[f8418,f2209]) ).
fof(f8481,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_40
| ~ spl54_66 ),
inference(forward_subsumption_resolution,[],[f8460,f2222]) ).
fof(f8484,plain,
( ! [X0] :
( rR(vd1329,sK5,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| sK4 = sK5
| vd1329 = sK5
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_39
| spl54_54
| spl54_69 ),
inference(forward_subsumption_resolution,[],[f8463,f2218]) ).
fof(f8485,plain,
( ! [X0] :
( vd684 != vangle(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| sK4 = sK5 )
| spl54_36
| spl54_37
| spl54_40
| ~ spl54_76 ),
inference(forward_subsumption_resolution,[],[f8464,f2205]) ).
fof(f8492,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_40
| ~ spl54_66 ),
inference(forward_subsumption_resolution,[],[f8481,f549]) ).
fof(f8495,plain,
( ! [X0] :
( rR(vd1329,sK5,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| vd1329 = sK5
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_39
| spl54_54
| spl54_69 ),
inference(forward_subsumption_resolution,[],[f8484,f858]) ).
fof(f8496,plain,
( ! [X0] :
( vd684 != vangle(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1303)
| sK4 = sK5 )
| spl54_36
| spl54_37
| spl54_40
| ~ spl54_76 ),
inference(forward_subsumption_resolution,[],[f8485,f549]) ).
fof(f8503,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| spl54_40
| ~ spl54_66 ),
inference(forward_subsumption_resolution,[],[f8492,f538]) ).
fof(f8506,plain,
( ! [X0] :
( rR(vd1329,sK5,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_39
| spl54_40
| spl54_54
| spl54_69 ),
inference(forward_subsumption_resolution,[],[f8495,f2222]) ).
fof(f8507,plain,
( ! [X0] :
( vd684 != vangle(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0)
| ~ rpoint(vd1303)
| sK4 = sK5 )
| spl54_36
| spl54_37
| spl54_40
| ~ spl54_76 ),
inference(forward_subsumption_resolution,[],[f8496,f547]) ).
fof(f8514,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0) )
| spl54_40
| ~ spl54_66 ),
inference(forward_subsumption_resolution,[],[f8503,f547]) ).
fof(f8517,plain,
( ! [X0] :
( rR(vd1329,sK5,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_39
| spl54_40
| spl54_54
| spl54_69 ),
inference(forward_subsumption_resolution,[],[f8506,f549]) ).
fof(f8518,plain,
( ! [X0] :
( vd684 != vangle(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0)
| sK4 = sK5 )
| spl54_36
| spl54_37
| spl54_40
| ~ spl54_76 ),
inference(forward_subsumption_resolution,[],[f8507,f541]) ).
fof(f8523,definition,
( spl54_126
<=> rR(sK4,sK5,vd1303) ),
introduced(definition,[new_symbols(definition,[spl54_126])],[avatar_definition]) ).
fof(f8524,plain,
( rR(sK4,sK5,vd1303)
| ~ spl54_126 ),
inference(avatar_component_clause,[],[f8523]) ).
fof(f8525,plain,
( ~ rR(sK4,sK5,vd1303)
| spl54_126 ),
inference(avatar_component_clause,[],[f8523]) ).
fof(f8530,plain,
( ! [X0] :
( rR(vd1329,sK5,sK4)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(vd1329)
| ~ rpoint(sK5) )
| spl54_39
| spl54_40
| spl54_54
| ~ spl54_66
| spl54_69 ),
inference(forward_subsumption_resolution,[],[f8517,f8514]) ).
fof(f8531,plain,
( ! [X0] :
( vd684 != vangle(sK4,vd1329,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0) )
| spl54_36
| spl54_37
| spl54_40
| ~ spl54_76 ),
inference(forward_subsumption_resolution,[],[f8518,f858]) ).
fof(f8537,definition,
( spl54_128
<=> vd684 = vangle(sK4,vd1329,sK6) ),
introduced(definition,[new_symbols(definition,[spl54_128])],[avatar_definition]) ).
fof(f8538,plain,
( vd684 = vangle(sK4,vd1329,sK6)
| ~ spl54_128 ),
inference(avatar_component_clause,[],[f8537]) ).
fof(f8539,plain,
( vd684 != vangle(sK4,vd1329,sK6)
| spl54_128 ),
inference(avatar_component_clause,[],[f8537]) ).
fof(f8545,plain,
( ! [X0] :
( rR(vd1329,sK5,sK4)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| spl54_39
| spl54_40
| spl54_54
| ~ spl54_66
| spl54_69 ),
inference(forward_subsumption_resolution,[],[f8530,f538]) ).
fof(f8547,definition,
( spl54_129
<=> vd684 = vangle(sK4,vd1329,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_129])],[avatar_definition]) ).
fof(f8548,plain,
( vd684 = vangle(sK4,vd1329,sK5)
| ~ spl54_129 ),
inference(avatar_component_clause,[],[f8547]) ).
fof(f8549,plain,
( vd684 != vangle(sK4,vd1329,sK5)
| spl54_129 ),
inference(avatar_component_clause,[],[f8547]) ).
fof(f8550,plain,
( spl54_51
| ~ spl54_129
| spl54_36
| spl54_37
| spl54_40
| ~ spl54_76 ),
inference(avatar_split_clause,[],[f8531,f4923,f2221,f2208,f2204,f8547,f3128]) ).
fof(f8553,plain,
( ! [X0] :
( rR(vd1329,sK5,sK4)
| ~ ron(vd1329,X0)
| ~ ron(sK5,X0)
| ~ rline(X0) )
| spl54_39
| spl54_40
| spl54_54
| ~ spl54_66
| spl54_69 ),
inference(forward_subsumption_resolution,[],[f8545,f547]) ).
fof(f8555,definition,
( spl54_130
<=> rR(vd1329,sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl54_130])],[avatar_definition]) ).
fof(f8556,plain,
( ~ rR(vd1329,sK5,sK4)
| spl54_130 ),
inference(avatar_component_clause,[],[f8555]) ).
fof(f8557,plain,
( rR(vd1329,sK5,sK4)
| ~ spl54_130 ),
inference(avatar_component_clause,[],[f8555]) ).
fof(f8559,plain,
( spl54_70
| spl54_130
| spl54_39
| spl54_40
| spl54_54
| ~ spl54_66
| spl54_69 ),
inference(avatar_split_clause,[],[f8553,f4221,f4135,f3143,f2221,f2217,f8555,f4561]) ).
fof(f8562,plain,
( ! [X0] :
( vd684 = vangle(sK4,vd1329,sK5)
| rR(vd1303,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK5
| vd1303 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) )
| spl54_40
| ~ spl54_50 ),
inference(forward_subsumption_resolution,[],[f7378,f3125]) ).
fof(f8597,plain,
( ! [X0] :
( vd684 = vangle(sK4,vd1329,sK5)
| rR(vd1303,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) )
| spl54_36
| spl54_40
| ~ spl54_50 ),
inference(forward_subsumption_resolution,[],[f8562,f2205]) ).
fof(f8623,plain,
( ! [X0] :
( vd684 = vangle(sK4,vd1329,sK5)
| rR(vd1303,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) )
| spl54_36
| spl54_37
| spl54_40
| ~ spl54_50 ),
inference(forward_subsumption_resolution,[],[f8597,f2209]) ).
fof(f8641,plain,
( ! [X0] :
( vd684 = vangle(sK4,vd1329,sK5)
| rR(vd1303,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) )
| spl54_36
| spl54_37
| spl54_40
| ~ spl54_50 ),
inference(forward_subsumption_resolution,[],[f8623,f547]) ).
fof(f8659,plain,
( ! [X0] :
( vd684 = vangle(sK4,vd1329,sK5)
| rR(vd1303,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0)
| ~ rpoint(vd1303) )
| spl54_36
| spl54_37
| spl54_40
| ~ spl54_50 ),
inference(forward_subsumption_resolution,[],[f8641,f549]) ).
fof(f8675,plain,
( ! [X0] :
( vd684 = vangle(sK4,vd1329,sK5)
| rR(vd1303,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0) )
| spl54_36
| spl54_37
| spl54_40
| ~ spl54_50 ),
inference(forward_subsumption_resolution,[],[f8659,f541]) ).
fof(f8691,definition,
( spl54_132
<=> rR(vd1303,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_132])],[avatar_definition]) ).
fof(f8693,plain,
( rR(vd1303,sK4,sK5)
| ~ spl54_132 ),
inference(avatar_component_clause,[],[f8691]) ).
fof(f8695,plain,
( spl54_51
| spl54_132
| spl54_129
| spl54_36
| spl54_37
| spl54_40
| ~ spl54_50 ),
inference(avatar_split_clause,[],[f8675,f3124,f2221,f2208,f2204,f8547,f8691,f3128]) ).
fof(f8756,plain,
( rR(sK4,sK5,vd1303)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1303)
| ~ spl54_65 ),
inference(resolution,[],[f4133,f1029]) ).
fof(f8758,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1303,X0)
| ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) )
| ~ spl54_65 ),
inference(resolution,[],[f4133,f1178]) ).
fof(f8786,plain,
( ~ rline(vd1297)
| ~ ron(vd1303,vd1297)
| ~ spl54_68 ),
inference(resolution,[],[f907,f4145]) ).
fof(f8787,plain,
( ~ rline(vd1297)
| ron(sK5,vd1297)
| ~ ron(vd1303,vd1297)
| ~ spl54_67 ),
inference(resolution,[],[f907,f4141]) ).
fof(f8792,plain,
( ron(sK5,vd1297)
| ~ ron(vd1303,vd1297)
| ~ spl54_67 ),
inference(forward_subsumption_resolution,[],[f8787,f628]) ).
fof(f8793,plain,
( ~ ron(vd1303,vd1297)
| ~ spl54_68 ),
inference(forward_subsumption_resolution,[],[f8786,f628]) ).
fof(f8795,plain,
( ~ ron(vd1303,vd1297)
| ~ spl54_64
| ~ spl54_67 ),
inference(forward_subsumption_resolution,[],[f8792,f4192]) ).
fof(f8796,plain,
( $false
| ~ spl54_68 ),
inference(forward_subsumption_resolution,[],[f8793,f905]) ).
fof(f8797,plain,
~ spl54_68,
inference(avatar_contradiction_clause,[],[f8796]) ).
fof(f8798,plain,
( $false
| ~ spl54_64
| ~ spl54_67 ),
inference(forward_subsumption_resolution,[],[f8795,f905]) ).
fof(f8799,plain,
( ~ spl54_64
| ~ spl54_67 ),
inference(avatar_contradiction_clause,[],[f8798]) ).
fof(f8803,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1303,X0)
| ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1303) )
| ~ spl54_65 ),
inference(forward_subsumption_resolution,[],[f8758,f547]) ).
fof(f8807,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1303,X0)
| ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(vd1303) )
| ~ spl54_65 ),
inference(forward_subsumption_resolution,[],[f8803,f549]) ).
fof(f8811,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1303,X0)
| ron(sK5,X0)
| ~ rline(X0) )
| ~ spl54_65 ),
inference(forward_subsumption_resolution,[],[f8807,f541]) ).
fof(f8815,plain,
( spl54_67
| ~ spl54_65 ),
inference(avatar_split_clause,[],[f8811,f4131,f4140]) ).
fof(f8823,plain,
( spl54_58
| ~ spl54_54 ),
inference(avatar_split_clause,[],[f3995,f3143,f3164]) ).
fof(f8874,plain,
( rR(sK5,sK4,vd1329)
| ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(vd1329)
| ~ spl54_69 ),
inference(resolution,[],[f4223,f1029]) ).
fof(f8882,plain,
( ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rpoint(vd1329)
| ~ spl54_54
| ~ spl54_69 ),
inference(forward_subsumption_resolution,[],[f8874,f3993]) ).
fof(f8893,plain,
( ~ rpoint(sK5)
| ~ rpoint(vd1329)
| ~ spl54_54
| ~ spl54_69 ),
inference(forward_subsumption_resolution,[],[f8882,f549]) ).
fof(f8899,plain,
( ~ rpoint(vd1329)
| ~ spl54_54
| ~ spl54_69 ),
inference(forward_subsumption_resolution,[],[f8893,f547]) ).
fof(f8903,plain,
( $false
| ~ spl54_54
| ~ spl54_69 ),
inference(forward_subsumption_resolution,[],[f8899,f538]) ).
fof(f8904,plain,
( ~ spl54_54
| ~ spl54_69 ),
inference(avatar_contradiction_clause,[],[f8903]) ).
fof(f8906,plain,
( spl54_49
| ~ spl54_45 ),
inference(avatar_split_clause,[],[f4010,f3075,f3119]) ).
fof(f8907,plain,
( $false
| ~ spl54_45
| ~ spl54_126 ),
inference(forward_subsumption_resolution,[],[f4008,f8524]) ).
fof(f8908,plain,
( ~ spl54_45
| ~ spl54_126 ),
inference(avatar_contradiction_clause,[],[f8907]) ).
fof(f8909,plain,
( $false
| ~ spl54_45
| ~ spl54_58
| ~ spl54_75 ),
inference(forward_subsumption_resolution,[],[f4023,f7129]) ).
fof(f8910,plain,
( ~ spl54_45
| ~ spl54_58
| ~ spl54_75 ),
inference(avatar_contradiction_clause,[],[f8909]) ).
fof(f8942,plain,
( ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1303)
| ~ spl54_65
| spl54_126 ),
inference(forward_subsumption_resolution,[],[f8756,f8525]) ).
fof(f8945,plain,
( ~ rpoint(sK4)
| ~ rpoint(vd1303)
| ~ spl54_65
| spl54_126 ),
inference(forward_subsumption_resolution,[],[f8942,f547]) ).
fof(f8946,plain,
( ~ rpoint(vd1303)
| ~ spl54_65
| spl54_126 ),
inference(forward_subsumption_resolution,[],[f8945,f549]) ).
fof(f8947,plain,
( $false
| ~ spl54_65
| spl54_126 ),
inference(forward_subsumption_resolution,[],[f8946,f541]) ).
fof(f8948,plain,
( ~ spl54_65
| spl54_126 ),
inference(avatar_contradiction_clause,[],[f8947]) ).
fof(f8949,plain,
( ~ spl54_49
| spl54_45 ),
inference(avatar_split_clause,[],[f4774,f3075,f3119]) ).
fof(f8952,plain,
( ~ spl54_61
| ~ spl54_56 ),
inference(avatar_split_clause,[],[f3948,f3152,f3940]) ).
fof(f8993,plain,
( ~ rline(vd1295)
| ~ ron(vd1329,vd1295)
| ~ spl54_70 ),
inference(resolution,[],[f4562,f909]) ).
fof(f9002,plain,
( ~ ron(vd1329,vd1295)
| ~ spl54_70 ),
inference(forward_subsumption_resolution,[],[f8993,f631]) ).
fof(f9011,plain,
( $false
| ~ spl54_70 ),
inference(forward_subsumption_resolution,[],[f9002,f621]) ).
fof(f9012,plain,
~ spl54_70,
inference(avatar_contradiction_clause,[],[f9011]) ).
fof(f9452,plain,
( ~ rR(vd1329,sK4,sK5)
| spl54_130 ),
inference(unit_resulting_resolution,[],[f1029,f549,f538,f547,f8556]) ).
fof(f9600,plain,
( ~ rR(vd1303,sK4,sK5)
| spl54_76 ),
inference(unit_resulting_resolution,[],[f1029,f549,f541,f547,f4924]) ).
fof(f9689,plain,
( ~ ron(sK5,vd1297)
| ~ spl54_51 ),
inference(unit_resulting_resolution,[],[f3129,f628,f905]) ).
fof(f9705,plain,
( ~ rline(vd1297)
| ~ ron(vd1329,vd1297)
| ~ spl54_60 ),
inference(resolution,[],[f3174,f907]) ).
fof(f9753,plain,
( ! [X0] :
( vd684 != vd684
| rR(vd1329,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| vd1329 = sK5
| vd1329 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_129 ),
inference(superposition,[],[f8549,f1132]) ).
fof(f9756,plain,
( ! [X0] :
( rR(vd1329,sK4,sK5)
| ~ ron(sK5,X0)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| vd1329 = sK5
| vd1329 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_129 ),
inference(trivial_inequality_removal,[],[f9753]) ).
fof(f10063,plain,
( vd684 != vangle(vd1329,sK6,sK4)
| spl54_21
| spl54_61 ),
inference(unit_resulting_resolution,[],[f1128,f545,f538,f549,f631,f863,f1789,f916,f621,f3942]) ).
fof(f10137,plain,
( vd684 != vangle(vd1329,sK6,vd1303)
| spl54_21
| spl54_39
| spl54_61 ),
inference(forward_demodulation,[],[f10063,f3899]) ).
fof(f11326,plain,
( vangle(sK5,sK6,sK4) = vangle(vd1329,sK6,sK5)
| spl54_21
| spl54_65 ),
inference(unit_resulting_resolution,[],[f999,f545,f547,f549,f538,f547,f631,f621,f916,f909,f902,f852,f863,f902,f1789,f4571,f2811,f4321,f4364]) ).
fof(f11394,plain,
( vd684 = vangle(sK5,sK6,sK4)
| spl54_21
| spl54_40
| spl54_65 ),
inference(forward_demodulation,[],[f11326,f2799]) ).
fof(f11418,plain,
( vd684 = vangle(vd1329,sK6,vd1303)
| spl54_21
| spl54_40
| spl54_65 ),
inference(backward_demodulation,[],[f2752,f11394]) ).
fof(f11428,plain,
( $false
| spl54_21
| spl54_39
| spl54_40
| spl54_61
| spl54_65 ),
inference(forward_subsumption_resolution,[],[f11418,f10137]) ).
fof(f11429,plain,
( spl54_21
| spl54_39
| spl54_40
| spl54_61
| spl54_65 ),
inference(avatar_contradiction_clause,[],[f11428]) ).
fof(f11572,plain,
( ~ rline(vd1295)
| ~ ron(vd1329,vd1297)
| ~ spl54_60
| ~ spl54_63 ),
inference(forward_demodulation,[],[f9705,f3966]) ).
fof(f11612,plain,
( ~ ron(sK5,vd1295)
| ~ spl54_51
| ~ spl54_63 ),
inference(forward_demodulation,[],[f9689,f3966]) ).
fof(f11666,plain,
( ~ ron(vd1329,vd1297)
| ~ spl54_60
| ~ spl54_63 ),
inference(forward_subsumption_resolution,[],[f11572,f631]) ).
fof(f11699,plain,
( $false
| ~ spl54_51
| ~ spl54_63 ),
inference(forward_subsumption_resolution,[],[f11612,f909]) ).
fof(f11700,plain,
( ~ spl54_51
| ~ spl54_63 ),
inference(avatar_contradiction_clause,[],[f11699]) ).
fof(f11716,plain,
( ~ ron(vd1329,vd1295)
| ~ spl54_60
| ~ spl54_63 ),
inference(forward_demodulation,[],[f11666,f3966]) ).
fof(f11736,plain,
( $false
| ~ spl54_60
| ~ spl54_63 ),
inference(forward_subsumption_resolution,[],[f11716,f621]) ).
fof(f11737,plain,
( ~ spl54_60
| ~ spl54_63 ),
inference(avatar_contradiction_clause,[],[f11736]) ).
fof(f11789,plain,
( ! [X0] :
( rR(vd1329,sK4,sK5)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| vd1329 = sK5
| vd1329 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| ~ spl54_59
| spl54_129 ),
inference(forward_subsumption_resolution,[],[f9756,f3170]) ).
fof(f11805,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| vd1329 = sK5
| vd1329 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| ~ spl54_59
| spl54_129
| spl54_130 ),
inference(forward_subsumption_resolution,[],[f11789,f9452]) ).
fof(f11816,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| vd1329 = sK4
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_40
| ~ spl54_59
| spl54_129
| spl54_130 ),
inference(forward_subsumption_resolution,[],[f11805,f2222]) ).
fof(f11827,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_39
| spl54_40
| ~ spl54_59
| spl54_129
| spl54_130 ),
inference(forward_subsumption_resolution,[],[f11816,f2218]) ).
fof(f11838,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_39
| spl54_40
| ~ spl54_59
| spl54_129
| spl54_130 ),
inference(forward_subsumption_resolution,[],[f11827,f547]) ).
fof(f11848,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ rpoint(vd1329) )
| spl54_39
| spl54_40
| ~ spl54_59
| spl54_129
| spl54_130 ),
inference(forward_subsumption_resolution,[],[f11838,f549]) ).
fof(f11860,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0) )
| spl54_39
| spl54_40
| ~ spl54_59
| spl54_129
| spl54_130 ),
inference(forward_subsumption_resolution,[],[f11848,f538]) ).
fof(f11861,plain,
( spl54_60
| spl54_39
| spl54_40
| ~ spl54_59
| spl54_129
| spl54_130 ),
inference(avatar_split_clause,[],[f11860,f8555,f8547,f3169,f2221,f2217,f3173]) ).
fof(f11870,plain,
( ~ spl54_76
| ~ spl54_49 ),
inference(avatar_split_clause,[],[f4062,f3119,f4923]) ).
fof(f11872,plain,
( $false
| spl54_76
| ~ spl54_132 ),
inference(forward_subsumption_resolution,[],[f9600,f8693]) ).
fof(f11873,plain,
( spl54_76
| ~ spl54_132 ),
inference(avatar_contradiction_clause,[],[f11872]) ).
fof(f11927,definition,
( spl54_185
<=> rR(vd1303,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_185])],[avatar_definition]) ).
fof(f11928,plain,
( ~ rR(vd1303,sK6,sK5)
| spl54_185 ),
inference(avatar_component_clause,[],[f11927]) ).
fof(f11929,plain,
( rR(vd1303,sK6,sK5)
| ~ spl54_185 ),
inference(avatar_component_clause,[],[f11927]) ).
fof(f12075,plain,
( rR(vd1303,sK5,sK6)
| ~ spl54_185 ),
inference(unit_resulting_resolution,[],[f1029,f545,f541,f547,f11929]) ).
fof(f12176,plain,
( vd684 != vangle(sK4,vd1329,sK5)
| spl54_39
| spl54_40
| ~ spl54_130 ),
inference(unit_resulting_resolution,[],[f2159,f631,f538,f547,f549,f909,f621,f858,f2222,f2218,f8557]) ).
fof(f12181,plain,
( rR(vd1329,sK4,sK5)
| ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5)
| ~ spl54_130 ),
inference(resolution,[],[f8557,f1029]) ).
fof(f12188,plain,
( ~ rpoint(sK4)
| ~ rpoint(vd1329)
| ~ rpoint(sK5)
| ~ spl54_58
| ~ spl54_130 ),
inference(forward_subsumption_resolution,[],[f12181,f4024]) ).
fof(f12195,plain,
( $false
| spl54_39
| spl54_40
| ~ spl54_129
| ~ spl54_130 ),
inference(forward_subsumption_resolution,[],[f12176,f8548]) ).
fof(f12196,plain,
( spl54_39
| spl54_40
| ~ spl54_129
| ~ spl54_130 ),
inference(avatar_contradiction_clause,[],[f12195]) ).
fof(f12201,plain,
( ~ rpoint(vd1329)
| ~ rpoint(sK5)
| ~ spl54_58
| ~ spl54_130 ),
inference(forward_subsumption_resolution,[],[f12188,f549]) ).
fof(f12207,plain,
( ~ rpoint(sK5)
| ~ spl54_58
| ~ spl54_130 ),
inference(forward_subsumption_resolution,[],[f12201,f538]) ).
fof(f12210,plain,
( $false
| ~ spl54_58
| ~ spl54_130 ),
inference(forward_subsumption_resolution,[],[f12207,f547]) ).
fof(f12211,plain,
( ~ spl54_58
| ~ spl54_130 ),
inference(avatar_contradiction_clause,[],[f12210]) ).
fof(f12239,definition,
( spl54_187
<=> rR(vd1329,sK4,sK6) ),
introduced(definition,[new_symbols(definition,[spl54_187])],[avatar_definition]) ).
fof(f12240,plain,
( ~ rR(vd1329,sK4,sK6)
| spl54_187 ),
inference(avatar_component_clause,[],[f12239]) ).
fof(f12241,plain,
( rR(vd1329,sK4,sK6)
| ~ spl54_187 ),
inference(avatar_component_clause,[],[f12239]) ).
fof(f12437,plain,
( vd684 != vangle(sK6,vd1329,sK4)
| spl54_21
| spl54_39
| ~ spl54_61
| ~ spl54_187 ),
inference(unit_resulting_resolution,[],[f2159,f631,f538,f549,f545,f1789,f2218,f863,f621,f12241,f3941]) ).
fof(f12535,plain,
( vd684 != vangle(sK4,vd1329,sK6)
| spl54_21
| spl54_39
| ~ spl54_61
| ~ spl54_187 ),
inference(forward_demodulation,[],[f12437,f2115]) ).
fof(f13140,plain,
( ~ rR(vd1303,sK5,sK6)
| ~ rpoint(sK6)
| ~ rpoint(vd1303)
| ~ rpoint(sK5)
| ~ spl54_49 ),
inference(resolution,[],[f4065,f1018]) ).
fof(f13143,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(vd1303) )
| ~ spl54_49 ),
inference(resolution,[],[f4065,f1178]) ).
fof(f13148,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1303) )
| ~ spl54_49 ),
inference(forward_subsumption_resolution,[],[f13143,f545]) ).
fof(f13150,plain,
( ~ rpoint(sK6)
| ~ rpoint(vd1303)
| ~ rpoint(sK5)
| ~ spl54_49
| ~ spl54_185 ),
inference(forward_subsumption_resolution,[],[f13140,f12075]) ).
fof(f13165,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(vd1303) )
| ~ spl54_49 ),
inference(forward_subsumption_resolution,[],[f13148,f547]) ).
fof(f13166,plain,
( ~ rpoint(vd1303)
| ~ rpoint(sK5)
| ~ spl54_49
| ~ spl54_185 ),
inference(forward_subsumption_resolution,[],[f13150,f545]) ).
fof(f13173,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ron(sK6,X0)
| ~ rline(X0) )
| ~ spl54_49 ),
inference(forward_subsumption_resolution,[],[f13165,f541]) ).
fof(f13174,plain,
( ~ rpoint(sK5)
| ~ spl54_49
| ~ spl54_185 ),
inference(forward_subsumption_resolution,[],[f13166,f541]) ).
fof(f13179,plain,
( $false
| ~ spl54_49
| ~ spl54_185 ),
inference(forward_subsumption_resolution,[],[f13174,f547]) ).
fof(f13180,plain,
( ~ spl54_49
| ~ spl54_185 ),
inference(avatar_contradiction_clause,[],[f13179]) ).
fof(f13191,plain,
( $false
| spl54_21
| spl54_39
| ~ spl54_61
| ~ spl54_128
| ~ spl54_187 ),
inference(forward_subsumption_resolution,[],[f12535,f8538]) ).
fof(f13192,plain,
( spl54_21
| spl54_39
| ~ spl54_61
| ~ spl54_128
| ~ spl54_187 ),
inference(avatar_contradiction_clause,[],[f13191]) ).
fof(f13201,plain,
( ! [X0] :
( vd684 != vd684
| ron(sK6,X0)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| vd1329 = sK6
| vd1329 = sK4
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| ~ spl54_128 ),
inference(superposition,[],[f1128,f8538]) ).
fof(f13204,plain,
( ! [X0] :
( ron(sK6,X0)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| vd1329 = sK6
| vd1329 = sK4
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| ~ spl54_128 ),
inference(trivial_inequality_removal,[],[f13201]) ).
fof(f13207,plain,
( ! [X0] :
( ron(sK6,X0)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| vd1329 = sK4
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| ~ spl54_128 ),
inference(forward_subsumption_resolution,[],[f13204,f863]) ).
fof(f13212,plain,
( ! [X0] :
( ron(sK6,X0)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_39
| ~ spl54_128 ),
inference(forward_subsumption_resolution,[],[f13207,f2218]) ).
fof(f13217,plain,
( ! [X0] :
( ron(sK6,X0)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_39
| ~ spl54_128 ),
inference(forward_subsumption_resolution,[],[f13212,f545]) ).
fof(f13222,plain,
( ! [X0] :
( ron(sK6,X0)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ rpoint(vd1329) )
| spl54_39
| ~ spl54_128 ),
inference(forward_subsumption_resolution,[],[f13217,f549]) ).
fof(f13227,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ron(sK6,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0) )
| spl54_39
| ~ spl54_128 ),
inference(forward_subsumption_resolution,[],[f13222,f538]) ).
fof(f13251,plain,
( ! [X0] :
( rR(sK4,vd1329,sK6)
| rR(sK6,vd1329,sK4)
| ~ ron(sK6,X0)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| sK4 = sK6
| vd1329 = sK6
| vd1329 = sK4
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_187 ),
inference(resolution,[],[f12240,f1174]) ).
fof(f13252,plain,
( ! [X0] :
( rR(sK4,vd1329,sK6)
| rR(sK6,vd1329,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| sK4 = sK6
| vd1329 = sK6
| vd1329 = sK4
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_39
| ~ spl54_128
| spl54_187 ),
inference(forward_subsumption_resolution,[],[f13251,f13227]) ).
fof(f13256,plain,
( ! [X0] :
( rR(sK6,vd1329,sK4)
| ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| sK4 = sK6
| vd1329 = sK6
| vd1329 = sK4
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_39
| ~ spl54_54
| ~ spl54_74
| ~ spl54_128
| spl54_187 ),
inference(forward_subsumption_resolution,[],[f13252,f7296]) ).
fof(f13258,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| sK4 = sK6
| vd1329 = sK6
| vd1329 = sK4
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_21
| spl54_39
| ~ spl54_54
| ~ spl54_61
| spl54_65
| ~ spl54_74
| ~ spl54_128
| spl54_187 ),
inference(forward_subsumption_resolution,[],[f13256,f7975]) ).
fof(f13260,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| vd1329 = sK6
| vd1329 = sK4
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_21
| spl54_39
| ~ spl54_54
| ~ spl54_61
| spl54_65
| ~ spl54_74
| ~ spl54_128
| spl54_187 ),
inference(forward_subsumption_resolution,[],[f13258,f1789]) ).
fof(f13262,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| vd1329 = sK4
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_21
| spl54_39
| ~ spl54_54
| ~ spl54_61
| spl54_65
| ~ spl54_74
| ~ spl54_128
| spl54_187 ),
inference(forward_subsumption_resolution,[],[f13260,f863]) ).
fof(f13264,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_21
| spl54_39
| ~ spl54_54
| ~ spl54_61
| spl54_65
| ~ spl54_74
| ~ spl54_128
| spl54_187 ),
inference(forward_subsumption_resolution,[],[f13262,f2218]) ).
fof(f13269,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(vd1329) )
| spl54_21
| spl54_39
| ~ spl54_54
| ~ spl54_61
| spl54_65
| ~ spl54_74
| ~ spl54_128
| spl54_187 ),
inference(forward_subsumption_resolution,[],[f13264,f545]) ).
fof(f13270,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0)
| ~ rpoint(vd1329) )
| spl54_21
| spl54_39
| ~ spl54_54
| ~ spl54_61
| spl54_65
| ~ spl54_74
| ~ spl54_128
| spl54_187 ),
inference(forward_subsumption_resolution,[],[f13269,f549]) ).
fof(f13271,plain,
( ! [X0] :
( ~ ron(sK4,X0)
| ~ ron(vd1329,X0)
| ~ rline(X0) )
| spl54_21
| spl54_39
| ~ spl54_54
| ~ spl54_61
| spl54_65
| ~ spl54_74
| ~ spl54_128
| spl54_187 ),
inference(forward_subsumption_resolution,[],[f13270,f538]) ).
fof(f13272,plain,
( spl54_60
| spl54_21
| spl54_39
| ~ spl54_54
| ~ spl54_61
| spl54_65
| ~ spl54_74
| ~ spl54_128
| spl54_187 ),
inference(avatar_split_clause,[],[f13271,f12239,f8537,f4912,f4131,f3940,f3143,f2217,f1787,f3173]) ).
fof(f13275,plain,
( ! [X0] :
( vd684 = vangle(sK4,vd1329,sK6)
| rR(vd1303,sK6,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK5
| vd1303 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(vd1303) )
| spl54_21
| ~ spl54_49 ),
inference(forward_subsumption_resolution,[],[f7693,f13173]) ).
fof(f13279,plain,
( ! [X0] :
( rR(vd1303,sK6,sK5)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK5
| vd1303 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(vd1303) )
| spl54_21
| ~ spl54_49
| spl54_128 ),
inference(forward_subsumption_resolution,[],[f13275,f8539]) ).
fof(f13282,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK5
| vd1303 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(vd1303) )
| spl54_21
| ~ spl54_49
| spl54_128
| spl54_185 ),
inference(forward_subsumption_resolution,[],[f13279,f11928]) ).
fof(f13284,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(vd1303) )
| spl54_21
| spl54_36
| ~ spl54_49
| spl54_128
| spl54_185 ),
inference(forward_subsumption_resolution,[],[f13282,f2205]) ).
fof(f13286,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(vd1303) )
| spl54_21
| spl54_36
| ~ spl54_49
| spl54_128
| spl54_185 ),
inference(forward_subsumption_resolution,[],[f13284,f867]) ).
fof(f13288,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(vd1303) )
| spl54_21
| spl54_36
| ~ spl54_49
| spl54_128
| spl54_185 ),
inference(forward_subsumption_resolution,[],[f13286,f547]) ).
fof(f13290,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0)
| ~ rpoint(vd1303) )
| spl54_21
| spl54_36
| ~ spl54_49
| spl54_128
| spl54_185 ),
inference(forward_subsumption_resolution,[],[f13288,f545]) ).
fof(f13292,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ ron(vd1303,X0)
| ~ rline(X0) )
| spl54_21
| spl54_36
| ~ spl54_49
| spl54_128
| spl54_185 ),
inference(forward_subsumption_resolution,[],[f13290,f541]) ).
fof(f13294,plain,
( spl54_51
| spl54_21
| spl54_36
| ~ spl54_49
| spl54_128
| spl54_185 ),
inference(avatar_split_clause,[],[f13292,f11927,f8537,f3119,f2204,f1787,f3128]) ).
fof(f13296,plain,
( vf(vd1329,sK4) = vf(vd1303,vd1303)
| ~ spl54_36 ),
inference(backward_demodulation,[],[f848,f2206]) ).
fof(f13926,plain,
( vd684 = vf(vd1329,sK4)
| ~ spl54_36 ),
inference(forward_demodulation,[],[f13296,f1922]) ).
fof(f14037,plain,
( $false
| ~ spl54_36
| spl54_39 ),
inference(forward_subsumption_resolution,[],[f13926,f3897]) ).
fof(f14038,plain,
( ~ spl54_36
| spl54_39 ),
inference(avatar_contradiction_clause,[],[f14037]) ).
cnf(s40,plain,
~ spl54_21,
inference(sat_conversion,[],[f1864]) ).
cnf(s51,plain,
( spl54_37
| spl54_38 ),
inference(sat_conversion,[],[f2235]) ).
cnf(s52,plain,
( spl54_40
| spl54_41 ),
inference(sat_conversion,[],[f2236]) ).
cnf(s53,plain,
~ spl54_37,
inference(sat_conversion,[],[f2355]) ).
cnf(s56,plain,
( spl54_37
| ~ spl54_40 ),
inference(sat_conversion,[],[f2611]) ).
cnf(s97,plain,
( spl54_36
| ~ spl54_38
| spl54_46
| spl54_47
| spl54_49 ),
inference(sat_conversion,[],[f3141]) ).
cnf(s104,plain,
( spl54_39
| spl54_54
| spl54_55
| spl54_56 ),
inference(sat_conversion,[],[f3162]) ).
cnf(s108,plain,
( spl54_39
| ~ spl54_41
| spl54_55
| spl54_56
| spl54_58 ),
inference(sat_conversion,[],[f3176]) ).
cnf(s109,plain,
( ~ spl54_36
| ~ spl54_39 ),
inference(sat_conversion,[],[f3381]) ).
cnf(s111,plain,
( spl54_36
| ~ spl54_39 ),
inference(sat_conversion,[],[f3586]) ).
cnf(s113,plain,
( spl54_63
| spl54_64 ),
inference(sat_conversion,[],[f3970]) ).
cnf(s114,plain,
( ~ spl54_47
| ~ spl54_63 ),
inference(sat_conversion,[],[f3980]) ).
cnf(s115,plain,
( spl54_61
| ~ spl54_63 ),
inference(sat_conversion,[],[f3985]) ).
cnf(s120,plain,
( spl54_37
| ~ spl54_66
| spl54_67 ),
inference(sat_conversion,[],[f4142]) ).
cnf(s121,plain,
( spl54_37
| ~ spl54_65
| ~ spl54_66
| spl54_68 ),
inference(sat_conversion,[],[f4146]) ).
cnf(s122,plain,
( spl54_37
| spl54_47
| spl54_65
| spl54_66 ),
inference(sat_conversion,[],[f4147]) ).
cnf(s128,plain,
( spl54_40
| spl54_56
| spl54_66
| spl54_69 ),
inference(sat_conversion,[],[f4224]) ).
cnf(s135,plain,
( spl54_21
| ~ spl54_61
| spl54_63 ),
inference(sat_conversion,[],[f4468]) ).
cnf(s147,plain,
( spl54_40
| ~ spl54_66
| ~ spl54_69
| spl54_70 ),
inference(sat_conversion,[],[f4563]) ).
cnf(s150,plain,
( ~ spl54_49
| spl54_50 ),
inference(sat_conversion,[],[f4709]) ).
cnf(s151,plain,
( ~ spl54_58
| spl54_59 ),
inference(sat_conversion,[],[f4710]) ).
cnf(s160,plain,
( spl54_40
| spl54_73
| spl54_74
| spl54_75 ),
inference(sat_conversion,[],[f4919]) ).
cnf(s161,plain,
( spl54_36
| spl54_37
| spl54_45
| spl54_65
| ~ spl54_67
| spl54_68
| spl54_76 ),
inference(sat_conversion,[],[f4926]) ).
cnf(s169,plain,
~ spl54_73,
inference(sat_conversion,[],[f5482]) ).
cnf(s240,plain,
( ~ spl54_46
| ~ spl54_55 ),
inference(sat_conversion,[],[f8453]) ).
cnf(s244,plain,
( spl54_36
| spl54_37
| spl54_40
| spl54_51
| ~ spl54_76
| ~ spl54_129 ),
inference(sat_conversion,[],[f8550]) ).
cnf(s247,plain,
( spl54_39
| spl54_40
| spl54_54
| ~ spl54_66
| spl54_69
| spl54_70
| spl54_130 ),
inference(sat_conversion,[],[f8559]) ).
cnf(s254,plain,
( spl54_36
| spl54_37
| spl54_40
| ~ spl54_50
| spl54_51
| spl54_129
| spl54_132 ),
inference(sat_conversion,[],[f8695]) ).
cnf(s272,plain,
~ spl54_68,
inference(sat_conversion,[],[f8797]) ).
cnf(s273,plain,
( ~ spl54_64
| ~ spl54_67 ),
inference(sat_conversion,[],[f8799]) ).
cnf(s274,plain,
( ~ spl54_65
| spl54_67 ),
inference(sat_conversion,[],[f8815]) ).
cnf(s278,plain,
( ~ spl54_54
| spl54_58 ),
inference(sat_conversion,[],[f8823]) ).
cnf(s305,plain,
( ~ spl54_54
| ~ spl54_69 ),
inference(sat_conversion,[],[f8904]) ).
cnf(s308,plain,
( ~ spl54_45
| spl54_49 ),
inference(sat_conversion,[],[f8906]) ).
cnf(s309,plain,
( ~ spl54_45
| ~ spl54_126 ),
inference(sat_conversion,[],[f8908]) ).
cnf(s310,plain,
( ~ spl54_45
| ~ spl54_58
| ~ spl54_75 ),
inference(sat_conversion,[],[f8910]) ).
cnf(s320,plain,
( ~ spl54_65
| spl54_126 ),
inference(sat_conversion,[],[f8948]) ).
cnf(s321,plain,
( spl54_45
| ~ spl54_49 ),
inference(sat_conversion,[],[f8949]) ).
cnf(s324,plain,
( ~ spl54_56
| ~ spl54_61 ),
inference(sat_conversion,[],[f8952]) ).
cnf(s332,plain,
~ spl54_70,
inference(sat_conversion,[],[f9012]) ).
cnf(s388,plain,
( spl54_21
| spl54_39
| spl54_40
| spl54_61
| spl54_65 ),
inference(sat_conversion,[],[f11429]) ).
cnf(s441,plain,
( ~ spl54_51
| ~ spl54_63 ),
inference(sat_conversion,[],[f11700]) ).
cnf(s443,plain,
( ~ spl54_60
| ~ spl54_63 ),
inference(sat_conversion,[],[f11737]) ).
cnf(s453,plain,
( spl54_39
| spl54_40
| ~ spl54_59
| spl54_60
| spl54_129
| spl54_130 ),
inference(sat_conversion,[],[f11861]) ).
cnf(s458,plain,
( ~ spl54_49
| ~ spl54_76 ),
inference(sat_conversion,[],[f11870]) ).
cnf(s459,plain,
( spl54_76
| ~ spl54_132 ),
inference(sat_conversion,[],[f11873]) ).
cnf(s469,plain,
( spl54_39
| spl54_40
| ~ spl54_129
| ~ spl54_130 ),
inference(sat_conversion,[],[f12196]) ).
cnf(s470,plain,
( ~ spl54_58
| ~ spl54_130 ),
inference(sat_conversion,[],[f12211]) ).
cnf(s489,plain,
( ~ spl54_49
| ~ spl54_185 ),
inference(sat_conversion,[],[f13180]) ).
cnf(s491,plain,
( spl54_21
| spl54_39
| ~ spl54_61
| ~ spl54_128
| ~ spl54_187 ),
inference(sat_conversion,[],[f13192]) ).
cnf(s493,plain,
( spl54_21
| spl54_39
| ~ spl54_54
| spl54_60
| ~ spl54_61
| spl54_65
| ~ spl54_74
| ~ spl54_128
| spl54_187 ),
inference(sat_conversion,[],[f13272]) ).
cnf(s496,plain,
( spl54_21
| spl54_36
| ~ spl54_49
| spl54_51
| spl54_128
| spl54_185 ),
inference(sat_conversion,[],[f13294]) ).
cnf(s509,plain,
( ~ spl54_36
| spl54_39 ),
inference(sat_conversion,[],[f14038]) ).
cnf(s518,plain,
( spl54_39
| spl54_40
| spl54_54
| ~ spl54_66
| spl54_69
| spl54_130 ),
inference(rat,[],[s247,s332]) ).
cnf(s530,plain,
( spl54_36
| spl54_37
| spl54_45
| spl54_65
| ~ spl54_67
| spl54_76 ),
inference(rat,[],[s161,s272]) ).
cnf(s531,plain,
( spl54_40
| spl54_74
| spl54_75 ),
inference(rat,[],[s160,s169]) ).
cnf(s533,plain,
( spl54_40
| ~ spl54_66
| ~ spl54_69 ),
inference(rat,[],[s147,s332]) ).
cnf(s536,plain,
( spl54_37
| ~ spl54_65
| ~ spl54_66 ),
inference(rat,[],[s121,s272]) ).
cnf(s543,plain,
~ spl54_40,
inference(rat,[],[s56,s53]) ).
cnf(s545,plain,
spl54_41,
inference(rat,[],[s52,s543]) ).
cnf(s546,plain,
spl54_38,
inference(rat,[],[s51,s53]) ).
cnf(s556,plain,
( spl54_63
| spl54_39 ),
inference(rat,[],[s274,s388,s273,s135,s113,s543,s40]) ).
cnf(s557,plain,
( spl54_45
| spl54_36 ),
inference(rat,[],[s530,s244,s536,s120,s453,s128,s151,s470,s305,s108,s104,s240,s97,s321,s443,s441,s114,s324,s115,s556,s111,s53,s543,s545,s546]) ).
cnf(s558,plain,
spl54_36,
inference(rat,[],[s531,s310,s493,s278,s518,s469,s254,s533,s491,s459,s122,s496,s150,s458,s489,s320,s308,s309,s557,s114,s115,s441,s443,s556,s111,s543,s40,s53]) ).
cnf(s559,plain,
spl54_39,
inference(rat,[],[s509,s558]) ).
cnf(s561,plain,
$false,
inference(rat,[],[s109,s559,s558]) ).
fof(f14167,plain,
$false,
inference(avatar_sat_refutation,[],[s561]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO328+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n009.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 08:06:15 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.42 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
% 12.18/2.63 % (1709756)Detected formulas, will run a generic FOF schedule.
% 12.18/2.63 % (1709766)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4159980360:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.18/2.63 % (1709764)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=164293401:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.18/2.63 % (1709761)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=776228609:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.18/2.63 % (1709762)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=2431714191:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.18/2.63 % (1709763)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=601136175:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.18/2.63 % (1709767)dis-21_1_sil=8000:lcm=predicate:random_seed=110914206: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)
% 12.18/2.63 % (1709765)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2756225544:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.18/2.63 % (1709766)Instruction limit reached!
% 12.18/2.63 % (1709766)------------------------------
% 12.18/2.63 % (1709766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/2.63 % (1709766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.63 % (1709766)CaDiCaL version: 2.1.3
% 12.18/2.63 % (1709766)Termination reason: Instruction limit
% 12.18/2.63 % (1709766)Termination phase: Saturation
% 12.18/2.63 % (1709766)Time elapsed: 0.048 s
% 12.18/2.63 % (1709766)Peak memory usage: 90 MB
% 12.18/2.63 % (1709766)Instructions burned: 142 (million)
% 12.18/2.63 % (1709764)Instruction limit reached!
% 12.18/2.63 % (1709764)------------------------------
% 12.18/2.63 % (1709764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/2.63 % (1709764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.63 % (1709764)CaDiCaL version: 2.1.3
% 12.18/2.63 % (1709764)Termination reason: Instruction limit
% 12.18/2.63 % (1709764)Termination phase: Saturation
% 12.18/2.63 % (1709764)Time elapsed: 0.056 s
% 12.18/2.63 % (1709764)Peak memory usage: 89 MB
% 12.18/2.63 % (1709764)Instructions burned: 110 (million)
% 12.18/2.63 % (1709765)Instruction limit reached!
% 12.18/2.63 % (1709765)------------------------------
% 12.18/2.63 % (1709765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/2.63 % (1709765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.63 % (1709765)CaDiCaL version: 2.1.3
% 12.18/2.63 % (1709765)Termination reason: Instruction limit
% 12.18/2.63 % (1709765)Termination phase: Saturation
% 12.18/2.63 % (1709765)Time elapsed: 0.059 s
% 12.18/2.63 % (1709765)Peak memory usage: 89 MB
% 12.18/2.63 % (1709765)Instructions burned: 121 (million)
% 12.18/2.63 % (1709767)Instruction limit reached!
% 12.18/2.63 % (1709767)------------------------------
% 12.18/2.63 % (1709767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/2.63 % (1709767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.63 % (1709767)CaDiCaL version: 2.1.3
% 12.18/2.63 % (1709767)Termination reason: Instruction limit
% 12.18/2.63 % (1709767)Termination phase: Saturation
% 12.18/2.63 % (1709767)Time elapsed: 0.069 s
% 12.18/2.63 % (1709767)Peak memory usage: 90 MB
% 12.18/2.63 % (1709767)Instructions burned: 130 (million)
% 12.18/2.63 % (1709775)lrs+10_1_sil=8000:sp=occurrence:random_seed=3874323566:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 12.18/2.63 % (1709775)Instruction limit reached!
% 12.18/2.63 % (1709775)------------------------------
% 12.18/2.63 % (1709775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/2.63 % (1709775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.63 % (1709775)CaDiCaL version: 2.1.3
% 12.18/2.63 % (1709775)Termination reason: Instruction limit
% 12.18/2.63 % (1709775)Termination phase: Saturation
% 12.18/2.63 % (1709775)Time elapsed: 0.074 s
% 12.18/2.63 % (1709775)Peak memory usage: 91 MB
% 12.18/2.63 % (1709775)Instructions burned: 286 (million)
% 18.14/3.48 % (1709776)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1254272824:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 18.14/3.48 % (1709777)lrs+1011_1_sil=32000:sp=occurrence:random_seed=120407112:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 18.14/3.48 % (1709778)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=1533507532:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 18.14/3.48 % (1709776)Instruction limit reached!
% 18.14/3.48 % (1709776)------------------------------
% 18.14/3.48 % (1709776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.48 % (1709776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.48 % (1709776)CaDiCaL version: 2.1.3
% 18.14/3.48 % (1709776)Termination reason: Instruction limit
% 18.14/3.48 % (1709776)Termination phase: Saturation
% 18.14/3.48 % (1709776)Time elapsed: 0.077 s
% 18.14/3.48 % (1709776)Peak memory usage: 90 MB
% 18.14/3.48 % (1709776)Instructions burned: 160 (million)
% 18.14/3.48 % (1709780)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2410137637:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 18.14/3.48 % (1709778)Instruction limit reached!
% 18.14/3.48 % (1709778)------------------------------
% 18.14/3.48 % (1709778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.48 % (1709778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.48 % (1709778)CaDiCaL version: 2.1.3
% 18.14/3.48 % (1709778)Termination reason: Instruction limit
% 18.14/3.48 % (1709778)Termination phase: Saturation
% 18.14/3.48 % (1709778)Time elapsed: 0.121 s
% 18.14/3.48 % (1709778)Peak memory usage: 90 MB
% 18.14/3.48 % (1709778)Instructions burned: 249 (million)
% 18.14/3.48 % (1709780)Instruction limit reached!
% 18.14/3.48 % (1709780)------------------------------
% 18.14/3.48 % (1709780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.48 % (1709780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.48 % (1709780)CaDiCaL version: 2.1.3
% 18.14/3.48 % (1709780)Termination reason: Instruction limit
% 18.14/3.48 % (1709780)Termination phase: Saturation
% 18.14/3.48 % (1709780)Time elapsed: 0.080 s
% 18.14/3.48 % (1709780)Peak memory usage: 89 MB
% 18.14/3.48 % (1709780)Instructions burned: 296 (million)
% 18.14/3.48 % (1709777)Instruction limit reached!
% 18.14/3.48 % (1709777)------------------------------
% 18.14/3.48 % (1709777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.48 % (1709777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.48 % (1709777)CaDiCaL version: 2.1.3
% 18.14/3.48 % (1709777)Termination reason: Instruction limit
% 18.14/3.48 % (1709777)Termination phase: Saturation
% 18.14/3.48 % (1709777)Time elapsed: 0.183 s
% 18.14/3.48 % (1709777)Peak memory usage: 91 MB
% 18.14/3.48 % (1709777)Instructions burned: 326 (million)
% 18.14/3.48 % (1709785)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3716572229:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 18.14/3.48 % (1709787)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2953267195:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 18.14/3.48 % (1709787)Refutation not found, incomplete strategy
% 18.14/3.48 % (1709787)------------------------------
% 18.14/3.48 % (1709787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.48 % (1709787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.48 % (1709787)CaDiCaL version: 2.1.3
% 18.14/3.48 % (1709787)Termination reason: Refutation not found, incomplete strategy
% 18.14/3.48 % (1709787)Time elapsed: 0.014 s
% 18.14/3.48 % (1709787)Peak memory usage: 89 MB
% 18.14/3.48 % (1709787)Instructions burned: 55 (million)
% 18.14/3.48 % (1709786)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1456068810:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 18.14/3.48 % (1709786)Instruction limit reached!
% 18.14/3.48 % (1709786)------------------------------
% 18.14/3.48 % (1709786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.48 % (1709786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.48 % (1709786)CaDiCaL version: 2.1.3
% 18.14/3.48 % (1709786)Termination reason: Instruction limit
% 18.14/3.48 % (1709786)Termination phase: Saturation
% 33.17/5.56 % (1709786)Time elapsed: 0.060 s
% 33.17/5.56 % (1709786)Peak memory usage: 90 MB
% 33.17/5.56 % (1709786)Instructions burned: 114 (million)
% 33.17/5.56 % (1709789)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=462424304:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 33.17/5.56 % (1709789)Instruction limit reached!
% 33.17/5.56 % (1709789)------------------------------
% 33.17/5.56 % (1709789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.17/5.56 % (1709789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.17/5.56 % (1709789)CaDiCaL version: 2.1.3
% 33.17/5.56 % (1709789)Termination reason: Instruction limit
% 33.17/5.56 % (1709789)Termination phase: Saturation
% 33.17/5.56 % (1709789)Time elapsed: 0.053 s
% 33.17/5.56 % (1709789)Peak memory usage: 89 MB
% 33.17/5.56 % (1709789)Instructions burned: 115 (million)
% 33.17/5.56 % (1709787)------------------------------
% 33.17/5.56 % (1709787)------------------------------
% 33.17/5.56 % (1709792)lrs+10_1_sil=8000:sp=occurrence:random_seed=2390261039:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 33.17/5.56 % (1709794)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1310070307:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 33.17/5.56 % (1709795)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2644828391:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 33.17/5.56 % (1709794)Refutation not found, incomplete strategy
% 33.17/5.56 % (1709794)------------------------------
% 33.17/5.56 % (1709794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.17/5.56 % (1709794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.17/5.56 % (1709794)CaDiCaL version: 2.1.3
% 33.17/5.56 % (1709794)Termination reason: Refutation not found, incomplete strategy
% 33.17/5.56 % (1709794)Time elapsed: 0.018 s
% 33.17/5.56 % (1709794)Peak memory usage: 89 MB
% 33.17/5.56 % (1709794)Instructions burned: 34 (million)
% 33.17/5.56 % (1709794)------------------------------
% 33.17/5.56 % (1709794)------------------------------
% 33.17/5.56 % (1709792)Instruction limit reached!
% 33.17/5.56 % (1709792)------------------------------
% 33.17/5.56 % (1709792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.17/5.56 % (1709792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.17/5.56 % (1709792)CaDiCaL version: 2.1.3
% 33.17/5.56 % (1709792)Termination reason: Instruction limit
% 33.17/5.56 % (1709792)Termination phase: Saturation
% 33.17/5.56 % (1709792)Time elapsed: 0.420 s
% 33.17/5.56 % (1709792)Peak memory usage: 94 MB
% 33.17/5.56 % (1709792)Instructions burned: 907 (million)
% 33.17/5.56 % (1709799)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=131321791:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 33.17/5.56 % (1709799)Instruction limit reached!
% 33.17/5.56 % (1709799)------------------------------
% 33.17/5.56 % (1709799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.17/5.56 % (1709799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.17/5.56 % (1709799)CaDiCaL version: 2.1.3
% 33.17/5.56 % (1709799)Termination reason: Instruction limit
% 33.17/5.56 % (1709799)Termination phase: Saturation
% 33.17/5.56 % (1709799)Time elapsed: 0.066 s
% 33.17/5.56 % (1709799)Peak memory usage: 93 MB
% 33.17/5.56 % (1709799)Instructions burned: 135 (million)
% 33.17/5.56 % (1709800)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=145814219:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 33.17/5.56 % (1709802)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1978686618:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 33.17/5.56 % (1709800)Instruction limit reached!
% 33.17/5.56 % (1709800)------------------------------
% 33.17/5.56 % (1709800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.17/5.56 % (1709800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.17/5.56 % (1709800)CaDiCaL version: 2.1.3
% 33.17/5.56 % (1709800)Termination reason: Instruction limit
% 33.17/5.56 % (1709800)Termination phase: Saturation
% 33.17/5.56 % (1709800)Time elapsed: 0.297 s
% 33.17/5.56 % (1709800)Peak memory usage: 93 MB
% 33.17/5.56 % (1709800)Instructions burned: 593 (million)
% 33.17/5.56 % (1709805)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=1001189764:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 35.60/5.98 % (1709805)Instruction limit reached!
% 35.60/5.98 % (1709805)------------------------------
% 35.60/5.98 % (1709805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.98 % (1709805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.98 % (1709805)CaDiCaL version: 2.1.3
% 35.60/5.98 % (1709805)Termination reason: Instruction limit
% 35.60/5.98 % (1709805)Termination phase: Saturation
% 35.60/5.98 % (1709805)Time elapsed: 0.065 s
% 35.60/5.98 % (1709805)Peak memory usage: 90 MB
% 35.60/5.98 % (1709805)Instructions burned: 126 (million)
% 35.60/5.98 % (1709807)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3737931538:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 35.60/5.98 % (1709785)Instruction limit reached!
% 35.60/5.98 % (1709785)------------------------------
% 35.60/5.98 % (1709785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.98 % (1709785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.98 % (1709785)CaDiCaL version: 2.1.3
% 35.60/5.98 % (1709785)Termination reason: Instruction limit
% 35.60/5.98 % (1709785)Termination phase: Saturation
% 35.60/5.98 % (1709785)Time elapsed: 1.499 s
% 35.60/5.98 % (1709785)Peak memory usage: 142 MB
% 35.60/5.98 % (1709785)Instructions burned: 2351 (million)
% 35.60/5.98 % (1709807)Instruction limit reached!
% 35.60/5.98 % (1709807)------------------------------
% 35.60/5.98 % (1709807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.98 % (1709807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.98 % (1709807)CaDiCaL version: 2.1.3
% 35.60/5.98 % (1709807)Termination reason: Instruction limit
% 35.60/5.98 % (1709807)Termination phase: Saturation
% 35.60/5.98 % (1709807)Time elapsed: 0.077 s
% 35.60/5.98 % (1709807)Peak memory usage: 91 MB
% 35.60/5.98 % (1709807)Instructions burned: 135 (million)
% 35.60/5.98 % (1709809)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4061600176:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 35.60/5.98 % (1709809)Refutation not found, incomplete strategy
% 35.60/5.98 % (1709809)------------------------------
% 35.60/5.98 % (1709809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.98 % (1709809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.98 % (1709809)CaDiCaL version: 2.1.3
% 35.60/5.98 % (1709809)Termination reason: Refutation not found, incomplete strategy
% 35.60/5.98 % (1709809)Time elapsed: 0.004 s
% 35.60/5.98 % (1709809)Peak memory usage: 88 MB
% 35.60/5.98 % (1709809)Instructions burned: 6 (million)
% 35.60/5.98 % (1709810)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=561715459:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi)
% 35.60/5.98 % (1709810)Refutation not found, incomplete strategy
% 35.60/5.98 % (1709810)------------------------------
% 35.60/5.98 % (1709810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.98 % (1709810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.98 % (1709810)CaDiCaL version: 2.1.3
% 35.60/5.98 % (1709810)Termination reason: Refutation not found, incomplete strategy
% 35.60/5.98 % (1709810)Time elapsed: 0.007 s
% 35.60/5.98 % (1709810)Peak memory usage: 88 MB
% 35.60/5.98 % (1709810)Instructions burned: 11 (million)
% 35.60/5.98 % (1709809)------------------------------
% 35.60/5.98 % (1709809)------------------------------
% 35.60/5.98 % (1709810)------------------------------
% 35.60/5.98 % (1709810)------------------------------
% 35.60/5.98 % (1709814)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=1388732430:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2975 on theBenchmark for (2975ds/150Mi)
% 35.60/5.98 % (1709813)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=2899672889:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 35.60/5.98 % (1709814)Instruction limit reached!
% 35.60/5.98 % (1709814)------------------------------
% 35.60/5.98 % (1709814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.98 % (1709814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.98 % (1709814)CaDiCaL version: 2.1.3
% 35.60/5.98 % (1709814)Termination reason: Instruction limit
% 35.60/5.98 % (1709814)Termination phase: Saturation
% 35.60/5.98 % (1709814)Time elapsed: 0.075 s
% 35.60/5.98 % (1709814)Peak memory usage: 92 MB
% 35.60/5.98 % (1709814)Instructions burned: 151 (million)
% 35.60/5.98 % (1709817)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1435633842:i=14155:bd=all_2973 on theBenchmark for (2973ds/14155Mi)
% 35.60/5.98 % (1709795)Instruction limit reached!
% 35.60/5.98 % (1709795)------------------------------
% 35.60/5.98 % (1709795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.98 % (1709795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.98 % (1709795)CaDiCaL version: 2.1.3
% 35.60/5.98 % (1709795)Termination reason: Instruction limit
% 35.60/5.98 % (1709795)Termination phase: Saturation
% 35.60/5.98 % (1709795)Time elapsed: 2.429 s
% 35.60/5.98 % (1709795)Peak memory usage: 140 MB
% 35.60/5.98 % (1709795)Instructions burned: 5203 (million)
% 35.60/5.98 % (1709819)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4012886784:i=667:av=off:fsr=off_2966 on theBenchmark for (2966ds/667Mi)
% 35.60/5.98 % (1709819)Refutation not found, incomplete strategy
% 35.60/5.98 % (1709819)------------------------------
% 35.60/5.98 % (1709819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.98 % (1709819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.98 % (1709819)CaDiCaL version: 2.1.3
% 35.60/5.98 % (1709819)Termination reason: Refutation not found, incomplete strategy
% 35.60/5.98 % (1709819)Time elapsed: 0.023 s
% 35.60/5.98 % (1709819)Peak memory usage: 89 MB
% 35.60/5.98 % (1709819)Instructions burned: 47 (million)
% 35.60/5.98 % (1709819)------------------------------
% 35.60/5.98 % (1709819)------------------------------
% 35.60/5.98 % (1709821)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=2192259036:s2a=on:i=185:s2at=1.8:fdi=4_2962 on theBenchmark for (2962ds/185Mi)
% 35.60/5.98 % (1709821)Instruction limit reached!
% 35.60/5.98 % (1709821)------------------------------
% 35.60/5.98 % (1709821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.98 % (1709821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.98 % (1709821)CaDiCaL version: 2.1.3
% 35.60/5.98 % (1709821)Termination reason: Instruction limit
% 35.60/5.98 % (1709821)Termination phase: Saturation
% 35.60/5.98 % (1709821)Time elapsed: 0.095 s
% 35.60/5.98 % (1709821)Peak memory usage: 93 MB
% 35.60/5.98 % (1709821)Instructions burned: 187 (million)
% 35.60/5.98 % (1709823)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2994455778:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2960 on theBenchmark for (2960ds/193Mi)
% 35.60/5.98 % (1709823)Instruction limit reached!
% 35.60/5.98 % (1709823)------------------------------
% 35.60/5.98 % (1709823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.98 % (1709823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.98 % (1709823)CaDiCaL version: 2.1.3
% 35.60/5.98 % (1709823)Termination reason: Instruction limit
% 35.60/5.98 % (1709823)Termination phase: Saturation
% 35.60/5.98 % (1709823)Time elapsed: 0.107 s
% 35.60/5.98 % (1709823)Peak memory usage: 91 MB
% 35.60/5.98 % (1709823)Instructions burned: 195 (million)
% 35.60/5.98 % (1709825)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2783069468:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2957 on theBenchmark for (2957ds/4850Mi)
% 35.60/5.98 % (1709825)Refutation not found, incomplete strategy
% 35.60/5.98 % (1709825)------------------------------
% 35.60/5.98 % (1709825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.98 % (1709825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.98 % (1709825)CaDiCaL version: 2.1.3
% 35.60/5.98 % (1709825)Termination reason: Refutation not found, incomplete strategy
% 35.60/5.98 % (1709825)Time elapsed: 0.017 s
% 35.60/5.98 % (1709825)Peak memory usage: 89 MB
% 35.60/5.98 % (1709825)Instructions burned: 34 (million)
% 35.60/5.98 % (1709825)------------------------------
% 35.60/5.98 % (1709825)------------------------------
% 35.60/5.98 % (1709827)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3591601391:i=12111:sd=1:ss=included_2954 on theBenchmark for (2954ds/12111Mi)
% 35.60/5.98 % (1709817)First to succeed.
% 35.60/5.98 % (1709817)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1709756"
% 35.60/5.98 % (1709817)Refutation found. Thanks to Tanya!
% 35.60/5.98 % SZS status Theorem for theBenchmark
% 35.60/5.98 % SZS output start Proof for theBenchmark
% See solution above
% 36.72/6.08 % (1709817)------------------------------
% 36.72/6.08 % (1709817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.72/6.08 % (1709817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.72/6.08 % (1709817)CaDiCaL version: 2.1.3
% 36.72/6.08 % (1709817)Termination reason: Refutation
% 36.72/6.08 % (1709817)Time elapsed: 2.088 s
% 36.72/6.08 % (1709817)Peak memory usage: 143 MB
% 36.72/6.08 % (1709817)Instructions burned: 3462 (million)
% 36.72/6.08 % (1709817)------------------------------
% 36.72/6.08 % (1709817)------------------------------
% 36.72/6.08 % (1709756)Success in time 5.126 s
% 36.72/6.08 % Vampire exiting
%------------------------------------------------------------------------------