%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO329+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 : n008.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 50.69s 9.17s
% Output : Refutation 59.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 72
% Syntax : Number of formulae : 687 ( 115 unt; 38 def)
% Number of atoms : 3517 ( 982 equ)
% Maximal formula atoms : 26 ( 5 avg)
% Number of connectives : 4987 (2157 ~;2606 |; 166 &)
% ( 44 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 39 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 15 con; 0-3 aty)
% Number of variables : 1071 ( 0 sgn1027 !; 44 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vplus(vangle(vd1289,vd1288,vd1302),vangle(vd1287,vd1288,vd1289)) = vangle(vd1287,vd1288,vd1302),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(379, 1350, 0)') ).
fof(f2,negated_conjecture,
vplus(vangle(vd1289,vd1288,vd1302),vangle(vd1287,vd1288,vd1289)) != vangle(vd1287,vd1288,vd1302),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f12,axiom,
vangle(vd1287,vd1289,vd1329) = vangle(vd1287,vd1288,vd1302),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(conjunct2(375)), 1345, 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(f17,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(f26,axiom,
~ rR(vd1287,vd1289,vd1302),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','neg(neg(372))') ).
fof(f29,axiom,
vd1299 = vd1300,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(348, 4)') ).
fof(f30,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(f31,axiom,
rpoint(vd1300),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(348, 1)') ).
fof(f32,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(f37,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(f39,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(f40,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(f42,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( ron(X4,X3)
& X4 = X5
& rpoint(X5)
& rcenter(X2,X3)
& X0 = X1
& rpoint(X1) )
=> ( vf(X2,X0) = vf(X2,X4)
<=> ron(X0,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(184), 0), imp(cond(axiom(184), 0)))') ).
fof(f53,axiom,
vd1289 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(371)), 1338, 0)') ).
fof(f56,axiom,
vd1302 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(conjunct2(conjunct2(368))), 1334, 0)') ).
fof(f90,axiom,
ron(vd1288,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(s2(plural(346)), 0)') ).
fof(f91,axiom,
! [X0,X1,X2,X3,X4] :
( ( vf(X2,X0) = vf(X2,X1)
& ron(X1,X4)
& ron(X0,X3)
& rcenter(X2,X4)
& rcenter(X2,X3)
& ? [X5] :
( X1 = X5
& rpoint(X5) )
& ? [X6] :
( X0 = X6
& rpoint(X6) ) )
=> X3 = X4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))') ).
fof(f92,axiom,
! [X0,X1] :
( ( ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ? [X4] :
( vf(X0,X1) = X4
& rreal(X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(160), 0), imp(cond(axiom(160), 0)))') ).
fof(f101,axiom,
! [X0,X1] :
( ( X0 != X1
& ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ? [X4] :
( ron(X1,X4)
& rcenter(X0,X4)
& rcircle(X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(53), 0), imp(cond(axiom(53), 0)))') ).
fof(f102,axiom,
vd1288 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(371), 1337, 0)') ).
fof(f106,axiom,
ron(vd1302,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct2(349), 0)') ).
fof(f107,axiom,
ron(vd1299,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(349), 0)') ).
fof(f108,axiom,
ron(vd1289,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(s2(plural(347)), 0)') ).
fof(f109,axiom,
ron(vd1287,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(s1(plural(347)), 0)') ).
fof(f110,axiom,
rline(vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(347, 0)') ).
fof(f112,axiom,
rline(vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(346, 0)') ).
fof(f115,axiom,
! [X0,X1] :
( ( X0 = X1
& rreal(X1) )
=> vplus(X0,v0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(141), 0), imp(cond(axiom(141), 0)))') ).
fof(f116,axiom,
v0 = vd684,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(axiom(137), 2)') ).
fof(f117,axiom,
rreal(vd684),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(axiom(137), 1)') ).
fof(f119,axiom,
ron(vd1287,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(s1(plural(369)), 0)') ).
fof(f122,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(f135,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( X1 != X2
& ron(X2,X5)
& ron(X1,X5)
& rinside(X0,X5)
& ron(X2,X3)
& ron(X1,X3)
& ron(X0,X3)
& X5 = X6
& rcircle(X6)
& X3 = X4
& rline(X4)
& ? [X7] :
( X2 = X7
& rpoint(X7) )
& ? [X8] :
( X1 = X8
& rpoint(X8) )
& ? [X9] :
( X0 = X9
& rpoint(X9) ) )
=> rR(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(119), 0), imp(cond(axiom(119), 0)))') ).
fof(f146,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(f147,axiom,
! [X0,X1] :
( rcenter(X0,X1)
=> rinside(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))') ).
fof(f189,plain,
vplus(vangle(vd1289,vd1288,vd1302),vangle(vd1287,vd1288,vd1289)) != vangle(vd1287,vd1288,vd1302),
inference(flattening,[],[f2]) ).
fof(f198,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(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(flattening,[],[f198]) ).
fof(f200,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
<=> vangle(X2,X0,X4) = v0 )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f201,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,[],[f200]) ).
fof(f222,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,[],[f37]) ).
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(flattening,[],[f222]) ).
fof(f226,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,[],[f39]) ).
fof(f227,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,[],[f226]) ).
fof(f228,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,[],[f40]) ).
fof(f229,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,[],[f228]) ).
fof(f230,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( vf(X2,X0) = vf(X2,X4)
<=> ron(X0,X3) )
| ~ ron(X4,X3)
| X4 != X5
| ~ rpoint(X5)
| ~ rcenter(X2,X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(ennf_transformation,[],[f42]) ).
fof(f231,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( vf(X2,X0) = vf(X2,X4)
<=> ron(X0,X3) )
| ~ ron(X4,X3)
| X4 != X5
| ~ rpoint(X5)
| ~ rcenter(X2,X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(flattening,[],[f230]) ).
fof(f275,plain,
! [X0,X1,X2,X3,X4] :
( X3 = X4
| vf(X2,X0) != vf(X2,X1)
| ~ ron(X1,X4)
| ~ ron(X0,X3)
| ~ rcenter(X2,X4)
| ~ rcenter(X2,X3)
| ! [X5] :
( X1 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X0 != X6
| ~ rpoint(X6) ) ),
inference(ennf_transformation,[],[f91]) ).
fof(f276,plain,
! [X0,X1,X2,X3,X4] :
( X3 = X4
| vf(X2,X0) != vf(X2,X1)
| ~ ron(X1,X4)
| ~ ron(X0,X3)
| ~ rcenter(X2,X4)
| ~ rcenter(X2,X3)
| ! [X5] :
( X1 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X0 != X6
| ~ rpoint(X6) ) ),
inference(flattening,[],[f275]) ).
fof(f277,plain,
! [X0,X1] :
( ? [X4] :
( vf(X0,X1) = X4
& rreal(X4) )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f92]) ).
fof(f278,plain,
! [X0,X1] :
( ? [X4] :
( vf(X0,X1) = X4
& rreal(X4) )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f277]) ).
fof(f295,plain,
! [X0,X1] :
( ? [X4] :
( ron(X1,X4)
& rcenter(X0,X4)
& rcircle(X4) )
| X0 = X1
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f101]) ).
fof(f296,plain,
! [X0,X1] :
( ? [X4] :
( ron(X1,X4)
& rcenter(X0,X4)
& rcircle(X4) )
| X0 = X1
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f295]) ).
fof(f301,plain,
! [X0,X1] :
( vplus(X0,v0) = X0
| X0 != X1
| ~ rreal(X1) ),
inference(ennf_transformation,[],[f115]) ).
fof(f302,plain,
! [X0,X1] :
( vplus(X0,v0) = X0
| X0 != X1
| ~ rreal(X1) ),
inference(flattening,[],[f301]) ).
fof(f309,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,[],[f122]) ).
fof(f310,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,[],[f309]) ).
fof(f334,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( rR(X0,X1,X2)
| X1 = X2
| ~ ron(X2,X5)
| ~ ron(X1,X5)
| ~ rinside(X0,X5)
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| X5 != X6
| ~ rcircle(X6)
| X3 != X4
| ~ rline(X4)
| ! [X7] :
( X2 != X7
| ~ rpoint(X7) )
| ! [X8] :
( X1 != X8
| ~ rpoint(X8) )
| ! [X9] :
( X0 != X9
| ~ rpoint(X9) ) ),
inference(ennf_transformation,[],[f135]) ).
fof(f335,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( rR(X0,X1,X2)
| X1 = X2
| ~ ron(X2,X5)
| ~ ron(X1,X5)
| ~ rinside(X0,X5)
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| X5 != X6
| ~ rcircle(X6)
| X3 != X4
| ~ rline(X4)
| ! [X7] :
( X2 != X7
| ~ rpoint(X7) )
| ! [X8] :
( X1 != X8
| ~ rpoint(X8) )
| ! [X9] :
( X0 != X9
| ~ rpoint(X9) ) ),
inference(flattening,[],[f334]) ).
fof(f356,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,[],[f146]) ).
fof(f357,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,[],[f356]) ).
fof(f358,plain,
! [X0,X1] :
( rinside(X0,X1)
| ~ rcenter(X0,X1) ),
inference(ennf_transformation,[],[f147]) ).
fof(f446,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
| vangle(X2,X0,X4) != v0 )
& ( vangle(X2,X0,X4) = v0
| rR(X0,X2,X4)
| ~ ron(X4,X6) ) )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(nnf_transformation,[],[f201]) ).
fof(f447,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
| vangle(X2,X0,X4) != v0 )
& ( vangle(X2,X0,X4) = v0
| rR(X0,X2,X4)
| ~ ron(X4,X6) ) )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(flattening,[],[f446]) ).
fof(f451,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)],[f32]) ).
fof(f453,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( ( vf(X2,X0) = vf(X2,X4)
| ~ ron(X0,X3) )
& ( ron(X0,X3)
| vf(X2,X0) != vf(X2,X4) ) )
| ~ ron(X4,X3)
| X4 != X5
| ~ rpoint(X5)
| ~ rcenter(X2,X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(nnf_transformation,[],[f231]) ).
fof(f461,plain,
! [X0,X1] :
( ? [X2] :
( vf(X0,X1) = X2
& rreal(X2) )
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(rectify,[],[f278]) ).
fof(f462,plain,
! [X0,X1] :
( ( vf(X0,X1) = sK11(X0,X1)
& rreal(sK11(X0,X1)) )
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X2,sK11(X0,X1))],[f461]) ).
fof(f465,plain,
! [X0,X1] :
( ? [X2] :
( ron(X1,X2)
& rcenter(X0,X2)
& rcircle(X2) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(rectify,[],[f296]) ).
fof(f466,plain,
! [X0,X1] :
( ( ron(X1,sK14(X0,X1))
& rcenter(X0,sK14(X0,X1))
& rcircle(sK14(X0,X1)) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X2,sK14(X0,X1))],[f465]) ).
fof(f518,plain,
vplus(vangle(vd1289,vd1288,vd1302),vangle(vd1287,vd1288,vd1289)) != vangle(vd1287,vd1288,vd1302),
inference(cnf_transformation,[],[f189]) ).
fof(f539,plain,
vangle(vd1287,vd1288,vd1302) = vangle(vd1287,vd1289,vd1329),
inference(cnf_transformation,[],[f12]) ).
fof(f541,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,[],[f199]) ).
fof(f544,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( vangle(X2,X0,X4) = v0
| rR(X0,X2,X4)
| ~ ron(X4,X6)
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f447]) ).
fof(f545,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X4,X6)
| vangle(X2,X0,X4) != v0
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f447]) ).
fof(f546,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rR(X0,X2,X4)
| vangle(X2,X0,X4) != v0
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f447]) ).
fof(f556,plain,
~ rR(vd1287,vd1289,vd1302),
inference(cnf_transformation,[],[f26]) ).
fof(f559,plain,
vd1299 = vd1300,
inference(cnf_transformation,[],[f29]) ).
fof(f560,plain,
rR(vd1288,vd1287,vd1299),
inference(cnf_transformation,[],[f30]) ).
fof(f561,plain,
rpoint(vd1303),
inference(cnf_transformation,[],[f30]) ).
fof(f562,plain,
rR(vd1289,vd1287,vd1302),
inference(cnf_transformation,[],[f30]) ).
fof(f563,plain,
vd1302 = vd1303,
inference(cnf_transformation,[],[f30]) ).
fof(f564,plain,
rpoint(vd1300),
inference(cnf_transformation,[],[f31]) ).
fof(f565,plain,
rpoint(sK6),
inference(cnf_transformation,[],[f451]) ).
fof(f566,plain,
vd1287 = sK6,
inference(cnf_transformation,[],[f451]) ).
fof(f567,plain,
rpoint(sK5),
inference(cnf_transformation,[],[f451]) ).
fof(f568,plain,
vd1288 = sK5,
inference(cnf_transformation,[],[f451]) ).
fof(f569,plain,
rpoint(sK4),
inference(cnf_transformation,[],[f451]) ).
fof(f570,plain,
vd1289 = sK4,
inference(cnf_transformation,[],[f451]) ).
fof(f573,plain,
vd1289 != vd1288,
inference(cnf_transformation,[],[f451]) ).
fof(f574,plain,
vf(vd1287,vd1288) = vf(vd1287,vd1289),
inference(cnf_transformation,[],[f451]) ).
fof(f580,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,[],[f223]) ).
fof(f582,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,[],[f227]) ).
fof(f583,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,[],[f229]) ).
fof(f584,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,[],[f229]) ).
fof(f585,plain,
! [X2,X3,X0,X1,X4,X5] :
( X0 != X2
| ~ rR(X1,X0,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(cnf_transformation,[],[f229]) ).
fof(f586,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,[],[f229]) ).
fof(f588,plain,
! [X2,X3,X0,X1,X4,X5] :
( ron(X0,X3)
| vf(X2,X0) != vf(X2,X4)
| ~ ron(X4,X3)
| X4 != X5
| ~ rpoint(X5)
| ~ rcenter(X2,X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f453]) ).
fof(f618,plain,
vd1289 != vd1287,
inference(cnf_transformation,[],[f53]) ).
fof(f621,plain,
vd1302 != vd1287,
inference(cnf_transformation,[],[f56]) ).
fof(f655,plain,
ron(vd1288,vd1295),
inference(cnf_transformation,[],[f90]) ).
fof(f656,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( X3 = X4
| vf(X2,X0) != vf(X2,X1)
| ~ ron(X1,X4)
| ~ ron(X0,X3)
| ~ rcenter(X2,X4)
| ~ rcenter(X2,X3)
| X1 != X5
| ~ rpoint(X5)
| X0 != X6
| ~ rpoint(X6) ),
inference(cnf_transformation,[],[f276]) ).
fof(f658,plain,
! [X3,X0,X1,X4] :
( vf(X0,X1) = sK11(X0,X1)
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f462]) ).
fof(f674,plain,
! [X3,X0,X1,X4] :
( rcircle(sK14(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f466]) ).
fof(f675,plain,
! [X3,X0,X1,X4] :
( rcenter(X0,sK14(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f466]) ).
fof(f676,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK14(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f466]) ).
fof(f677,plain,
vd1288 != vd1287,
inference(cnf_transformation,[],[f102]) ).
fof(f681,plain,
ron(vd1302,vd1297),
inference(cnf_transformation,[],[f106]) ).
fof(f682,plain,
ron(vd1299,vd1295),
inference(cnf_transformation,[],[f107]) ).
fof(f683,plain,
ron(vd1289,vd1297),
inference(cnf_transformation,[],[f108]) ).
fof(f684,plain,
ron(vd1287,vd1297),
inference(cnf_transformation,[],[f109]) ).
fof(f685,plain,
rline(vd1297),
inference(cnf_transformation,[],[f110]) ).
fof(f687,plain,
rline(vd1295),
inference(cnf_transformation,[],[f112]) ).
fof(f690,plain,
! [X0,X1] :
( vplus(X0,v0) = X0
| X0 != X1
| ~ rreal(X1) ),
inference(cnf_transformation,[],[f302]) ).
fof(f691,plain,
v0 = vd684,
inference(cnf_transformation,[],[f116]) ).
fof(f692,plain,
rreal(vd684),
inference(cnf_transformation,[],[f117]) ).
fof(f694,plain,
ron(vd1287,vd1295),
inference(cnf_transformation,[],[f119]) ).
fof(f698,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,[],[f310]) ).
fof(f727,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( rR(X0,X1,X2)
| X1 = X2
| ~ ron(X2,X5)
| ~ ron(X1,X5)
| ~ rinside(X0,X5)
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| X5 != X6
| ~ rcircle(X6)
| X3 != X4
| ~ rline(X4)
| X2 != X7
| ~ rpoint(X7)
| X1 != X8
| ~ rpoint(X8)
| X0 != X9
| ~ rpoint(X9) ),
inference(cnf_transformation,[],[f335]) ).
fof(f738,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,[],[f357]) ).
fof(f739,plain,
! [X0,X1] :
( ~ rcenter(X0,X1)
| rinside(X0,X1) ),
inference(cnf_transformation,[],[f358]) ).
fof(f862,plain,
vplus(vangle(sK4,sK5,vd1303),vangle(sK6,sK5,sK4)) != vangle(sK6,sK5,vd1303),
inference(definition_unfolding,[],[f518,f570,f568,f563,f566,f568,f570,f566,f568,f563]) ).
fof(f868,plain,
vangle(sK6,sK5,vd1303) = vangle(sK6,sK4,vd1329),
inference(definition_unfolding,[],[f539,f566,f568,f563,f566,f570]) ).
fof(f872,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,[],[f546,f691]) ).
fof(f873,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,[],[f545,f691]) ).
fof(f874,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,[],[f544,f691]) ).
fof(f877,plain,
~ rR(sK6,sK4,vd1303),
inference(definition_unfolding,[],[f556,f566,f570,f563]) ).
fof(f879,plain,
rR(sK4,sK6,vd1303),
inference(definition_unfolding,[],[f562,f570,f566,f563]) ).
fof(f880,plain,
rR(sK5,sK6,vd1300),
inference(definition_unfolding,[],[f560,f568,f566,f559]) ).
fof(f881,plain,
vf(sK6,sK5) = vf(sK6,sK4),
inference(definition_unfolding,[],[f574,f566,f568,f566,f570]) ).
fof(f882,plain,
sK4 != sK5,
inference(definition_unfolding,[],[f573,f570,f568]) ).
fof(f892,plain,
sK4 != sK6,
inference(definition_unfolding,[],[f618,f570,f566]) ).
fof(f894,plain,
vd1303 != sK6,
inference(definition_unfolding,[],[f621,f563,f566]) ).
fof(f927,plain,
ron(sK5,vd1295),
inference(definition_unfolding,[],[f655,f568]) ).
fof(f928,plain,
sK5 != sK6,
inference(definition_unfolding,[],[f677,f568,f566]) ).
fof(f932,plain,
ron(vd1303,vd1297),
inference(definition_unfolding,[],[f681,f563]) ).
fof(f933,plain,
ron(vd1300,vd1295),
inference(definition_unfolding,[],[f682,f559]) ).
fof(f934,plain,
ron(sK4,vd1297),
inference(definition_unfolding,[],[f683,f570]) ).
fof(f935,plain,
ron(sK6,vd1297),
inference(definition_unfolding,[],[f684,f566]) ).
fof(f937,plain,
! [X0,X1] :
( vplus(X0,vd684) = X0
| X0 != X1
| ~ rreal(X1) ),
inference(definition_unfolding,[],[f690,f691]) ).
fof(f938,plain,
ron(sK6,vd1295),
inference(definition_unfolding,[],[f694,f566]) ).
fof(f1035,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,[],[f541]) ).
fof(f1036,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,[],[f1035]) ).
fof(f1037,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,[],[f1036]) ).
fof(f1038,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,[],[f1037]) ).
fof(f1039,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,[],[f1038]) ).
fof(f1040,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,[],[f1039]) ).
fof(f1041,plain,
! [X10,X11,X8,X9,X7,X12,X13] :
( ~ rline(X7)
| 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)
| vangle(X10,X13,X9) = vangle(X12,X13,X11)
| ~ rline(X8)
| ~ rpoint(X9)
| ~ rpoint(X10)
| ~ rpoint(X11)
| ~ rpoint(X12)
| ~ rpoint(X13) ),
inference(equality_resolution,[],[f1040]) ).
fof(f1042,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,[],[f872]) ).
fof(f1043,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,[],[f1042]) ).
fof(f1044,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,[],[f1043]) ).
fof(f1045,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,[],[f1044]) ).
fof(f1046,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,[],[f873]) ).
fof(f1047,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,[],[f1046]) ).
fof(f1048,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,[],[f1047]) ).
fof(f1049,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,[],[f1048]) ).
fof(f1050,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,[],[f874]) ).
fof(f1051,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,[],[f1050]) ).
fof(f1052,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,[],[f1051]) ).
fof(f1053,plain,
! [X3,X1,X7,X5] :
( ~ rline(X7)
| rR(X1,X3,X5)
| ~ ron(X5,X7)
| ~ ron(X3,X7)
| ~ ron(X1,X7)
| X1 = X5
| X1 = X3
| vd684 = vangle(X3,X1,X5)
| ~ rpoint(X5)
| ~ rpoint(X3)
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f1052]) ).
fof(f1092,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,[],[f580]) ).
fof(f1093,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,[],[f1092]) ).
fof(f1094,plain,
! [X3,X4,X5] :
( ~ rpoint(X5)
| X3 = X5
| X4 = X5
| ~ rpoint(X3)
| ~ rpoint(X4)
| vangle(X3,X4,X5) = vangle(X5,X4,X3) ),
inference(equality_resolution,[],[f1093]) ).
fof(f1098,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,[],[f582]) ).
fof(f1099,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,[],[f1098]) ).
fof(f1100,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,[],[f1099]) ).
fof(f1101,plain,
! [X6,X7,X4,X5] :
( ~ rpoint(X7)
| ~ rR(X5,X6,X4)
| ~ rR(X6,X7,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| rR(X6,X7,X4) ),
inference(equality_resolution,[],[f1100]) ).
fof(f1102,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,[],[f586]) ).
fof(f1103,plain,
! [X3,X0,X4,X5] :
( ~ rR(X0,X4,X3)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1102]) ).
fof(f1104,plain,
! [X3,X4,X5] :
( ~ rpoint(X5)
| ~ rR(X4,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rR(X5,X4,X3) ),
inference(equality_resolution,[],[f1103]) ).
fof(f1105,plain,
! [X2,X3,X1,X4,X5] :
( ~ rR(X1,X2,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f585]) ).
fof(f1106,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X3,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1105]) ).
fof(f1107,plain,
! [X3,X4,X5] :
( ~ rR(X4,X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1106]) ).
fof(f1108,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1107]) ).
fof(f1109,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,[],[f584]) ).
fof(f1110,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X1,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X1 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1109]) ).
fof(f1111,plain,
! [X3,X4,X5] :
( ~ rR(X4,X4,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X4 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1110]) ).
fof(f1112,plain,
! [X3,X5] :
( ~ rR(X5,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1111]) ).
fof(f1113,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,[],[f583]) ).
fof(f1114,plain,
! [X3,X0,X4,X5] :
( rR(X4,X3,X0)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1113]) ).
fof(f1115,plain,
! [X3,X4,X5] :
( ~ rR(X4,X5,X3)
| rR(X4,X3,X5)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1114]) ).
fof(f1118,plain,
! [X2,X3,X0,X1,X5] :
( ron(X0,X3)
| vf(X2,X0) != vf(X2,X5)
| ~ ron(X5,X3)
| ~ rpoint(X5)
| ~ rcenter(X2,X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f588]) ).
fof(f1119,plain,
! [X2,X3,X1,X5] :
( ~ rcenter(X2,X3)
| vf(X2,X1) != vf(X2,X5)
| ~ ron(X5,X3)
| ~ rpoint(X5)
| ron(X1,X3)
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f1118]) ).
fof(f1174,plain,
! [X2,X3,X0,X6,X4,X5] :
( X3 = X4
| vf(X2,X0) != vf(X2,X5)
| ~ ron(X5,X4)
| ~ ron(X0,X3)
| ~ rcenter(X2,X4)
| ~ rcenter(X2,X3)
| ~ rpoint(X5)
| X0 != X6
| ~ rpoint(X6) ),
inference(equality_resolution,[],[f656]) ).
fof(f1175,plain,
! [X2,X3,X6,X4,X5] :
( ~ rcenter(X2,X3)
| vf(X2,X5) != vf(X2,X6)
| ~ ron(X5,X4)
| ~ ron(X6,X3)
| ~ rcenter(X2,X4)
| X3 = X4
| ~ rpoint(X5)
| ~ rpoint(X6) ),
inference(equality_resolution,[],[f1174]) ).
fof(f1176,plain,
! [X3,X0,X4] :
( vf(X0,X3) = sK11(X0,X3)
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f658]) ).
fof(f1177,plain,
! [X3,X4] :
( ~ rpoint(X4)
| ~ rpoint(X3)
| vf(X4,X3) = sK11(X4,X3) ),
inference(equality_resolution,[],[f1176]) ).
fof(f1217,plain,
! [X3,X0,X4] :
( ron(X3,sK14(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f676]) ).
fof(f1218,plain,
! [X3,X4] :
( ron(X3,sK14(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1217]) ).
fof(f1219,plain,
! [X3,X0,X4] :
( rcenter(X0,sK14(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f675]) ).
fof(f1220,plain,
! [X3,X4] :
( rcenter(X4,sK14(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1219]) ).
fof(f1221,plain,
! [X3,X0,X4] :
( rcircle(sK14(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f674]) ).
fof(f1222,plain,
! [X3,X4] :
( rcircle(sK14(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1221]) ).
fof(f1228,plain,
! [X1] :
( ~ rreal(X1)
| vplus(X1,vd684) = X1 ),
inference(equality_resolution,[],[f937]) ).
fof(f1246,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,[],[f698]) ).
fof(f1247,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,[],[f1246]) ).
fof(f1248,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,[],[f1247]) ).
fof(f1249,plain,
! [X6,X7,X4,X5] :
( ~ rline(X4)
| ~ ron(X6,X4)
| ~ ron(X7,X4)
| ~ rR(X6,X7,X5)
| ron(X5,X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1248]) ).
fof(f1342,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4] :
( rR(X0,X1,X2)
| X1 = X2
| ~ ron(X2,X6)
| ~ ron(X1,X6)
| ~ rinside(X0,X6)
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rcircle(X6)
| X3 != X4
| ~ rline(X4)
| X2 != X7
| ~ rpoint(X7)
| X1 != X8
| ~ rpoint(X8)
| X0 != X9
| ~ rpoint(X9) ),
inference(equality_resolution,[],[f727]) ).
fof(f1343,plain,
! [X2,X0,X1,X8,X6,X9,X7,X4] :
( rR(X0,X1,X2)
| X1 = X2
| ~ ron(X2,X6)
| ~ ron(X1,X6)
| ~ rinside(X0,X6)
| ~ ron(X2,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rcircle(X6)
| ~ rline(X4)
| X2 != X7
| ~ rpoint(X7)
| X1 != X8
| ~ rpoint(X8)
| X0 != X9
| ~ rpoint(X9) ),
inference(equality_resolution,[],[f1342]) ).
fof(f1344,plain,
! [X0,X1,X8,X6,X9,X7,X4] :
( rR(X0,X1,X7)
| X1 = X7
| ~ ron(X7,X6)
| ~ ron(X1,X6)
| ~ rinside(X0,X6)
| ~ ron(X7,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rcircle(X6)
| ~ rline(X4)
| ~ rpoint(X7)
| X1 != X8
| ~ rpoint(X8)
| X0 != X9
| ~ rpoint(X9) ),
inference(equality_resolution,[],[f1343]) ).
fof(f1345,plain,
! [X0,X8,X6,X9,X7,X4] :
( rR(X0,X8,X7)
| X7 = X8
| ~ ron(X7,X6)
| ~ ron(X8,X6)
| ~ rinside(X0,X6)
| ~ ron(X7,X4)
| ~ ron(X8,X4)
| ~ ron(X0,X4)
| ~ rcircle(X6)
| ~ rline(X4)
| ~ rpoint(X7)
| ~ rpoint(X8)
| X0 != X9
| ~ rpoint(X9) ),
inference(equality_resolution,[],[f1344]) ).
fof(f1346,plain,
! [X8,X6,X9,X7,X4] :
( ~ rcircle(X6)
| X7 = X8
| ~ ron(X7,X6)
| ~ ron(X8,X6)
| ~ rinside(X9,X6)
| ~ ron(X7,X4)
| ~ ron(X8,X4)
| ~ ron(X9,X4)
| rR(X9,X8,X7)
| ~ rline(X4)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9) ),
inference(equality_resolution,[],[f1345]) ).
fof(f1395,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,[],[f738]) ).
fof(f1396,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,[],[f1395]) ).
fof(f1397,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,[],[f1396]) ).
fof(f1398,plain,
! [X6,X7,X4,X5] :
( ~ rpoint(X7)
| ~ rR(X4,X7,X6)
| ~ rR(X6,X7,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| rR(X4,X7,X5) ),
inference(equality_resolution,[],[f1397]) ).
fof(f1739,plain,
! [X3,X5] :
( ~ rR(X5,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X5) ),
inference(duplicate_literal_removal,[],[f1112]) ).
fof(f1740,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f1108]) ).
fof(f1816,definition,
( spl55_20
<=> vd1300 = sK6 ),
introduced(definition,[new_symbols(definition,[spl55_20])],[avatar_definition]) ).
fof(f1817,plain,
( vd1300 != sK6
| spl55_20 ),
inference(avatar_component_clause,[],[f1816]) ).
fof(f1821,definition,
( spl55_21
<=> sK4 = sK6 ),
introduced(definition,[new_symbols(definition,[spl55_21])],[avatar_definition]) ).
fof(f1822,plain,
( sK4 != sK6
| spl55_21 ),
inference(avatar_component_clause,[],[f1821]) ).
fof(f1827,definition,
( spl55_22
<=> rR(sK6,sK5,vd1300) ),
introduced(definition,[new_symbols(definition,[spl55_22])],[avatar_definition]) ).
fof(f1883,plain,
~ spl55_21,
inference(avatar_split_clause,[],[f892,f1821]) ).
fof(f1884,plain,
vplus(vangle(sK4,sK5,vd1303),vangle(sK6,sK5,sK4)) != vangle(sK6,sK4,vd1329),
inference(forward_demodulation,[],[f862,f868]) ).
fof(f1894,plain,
( rR(sK4,vd1303,sK6)
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(resolution,[],[f1115,f879]) ).
fof(f1895,plain,
( rR(sK5,vd1300,sK6)
| ~ rpoint(vd1300)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(resolution,[],[f1115,f880]) ).
fof(f1896,plain,
( rR(sK5,vd1300,sK6)
| ~ rpoint(sK5)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1895,f564]) ).
fof(f1897,plain,
( rR(sK4,vd1303,sK6)
| ~ rpoint(sK4)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1894,f561]) ).
fof(f1898,plain,
( rR(sK5,vd1300,sK6)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1896,f567]) ).
fof(f1899,plain,
( rR(sK4,vd1303,sK6)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f1897,f569]) ).
fof(f1900,plain,
rR(sK5,vd1300,sK6),
inference(forward_subsumption_resolution,[],[f1898,f565]) ).
fof(f1901,plain,
rR(sK4,vd1303,sK6),
inference(forward_subsumption_resolution,[],[f1899,f565]) ).
fof(f1912,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ rline(X5)
| rR(X0,X3,X4)
| X0 = X2
| X0 = X4
| X0 = X1
| X0 = X3
| ~ ron(X2,vd1297)
| ~ ron(X1,vd1297)
| ~ ron(X4,X5)
| ~ ron(X3,X5)
| ~ ron(X0,X5)
| vangle(X3,X0,X1) = vangle(X4,X0,X2)
| rR(X0,X1,X2)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0) ),
inference(resolution,[],[f685,f1041]) ).
fof(f1913,plain,
! [X2,X0,X1] :
( ~ ron(X2,vd1297)
| rR(X0,X1,X2)
| ~ ron(X1,vd1297)
| ~ ron(X0,vd1297)
| X0 = X2
| X0 = X1
| vangle(X1,X0,X2) = vd684
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f1053,f685]) ).
fof(f1914,plain,
! [X0,X1] :
( rR(X0,X1,vd1303)
| ~ ron(X1,vd1297)
| ~ ron(X0,vd1297)
| vd1303 = X0
| X0 = X1
| vd684 = vangle(X1,X0,vd1303)
| ~ rpoint(vd1303)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f1913,f932]) ).
fof(f1916,plain,
! [X0,X1] :
( rR(X0,X1,sK4)
| ~ ron(X1,vd1297)
| ~ ron(X0,vd1297)
| sK4 = X0
| X0 = X1
| vd684 = vangle(X1,X0,sK4)
| ~ rpoint(sK4)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f1913,f934]) ).
fof(f1917,plain,
! [X0,X1] :
( ~ ron(X1,vd1297)
| rR(X0,X1,sK4)
| ~ ron(X0,vd1297)
| sK4 = X0
| X0 = X1
| vd684 = vangle(X1,X0,sK4)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1916,f569]) ).
fof(f1919,plain,
! [X0,X1] :
( ~ ron(X1,vd1297)
| rR(X0,X1,vd1303)
| ~ ron(X0,vd1297)
| vd1303 = X0
| X0 = X1
| vd684 = vangle(X1,X0,vd1303)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1914,f561]) ).
fof(f1920,plain,
! [X2,X0,X1] :
( ~ ron(X2,vd1295)
| rR(X0,X1,X2)
| ~ ron(X1,vd1295)
| ~ ron(X0,vd1295)
| X0 = X2
| X0 = X1
| vangle(X1,X0,X2) = vd684
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f687,f1053]) ).
fof(f1923,plain,
! [X0,X1] :
( rR(X0,X1,sK6)
| ~ ron(X1,vd1295)
| ~ ron(X0,vd1295)
| sK6 = X0
| X0 = X1
| vd684 = vangle(X1,X0,sK6)
| ~ rpoint(sK6)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f1920,f938]) ).
fof(f1924,plain,
! [X0,X1] :
( ~ ron(X1,vd1295)
| rR(X0,X1,sK6)
| ~ ron(X0,vd1295)
| sK6 = X0
| X0 = X1
| vd684 = vangle(X1,X0,sK6)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1923,f565]) ).
fof(f1926,plain,
! [X0] :
( rR(X0,sK5,sK6)
| ~ ron(X0,vd1295)
| sK6 = X0
| sK5 = X0
| vd684 = vangle(sK5,X0,sK6)
| ~ rpoint(sK5)
| ~ rpoint(X0) ),
inference(resolution,[],[f1924,f927]) ).
fof(f1930,plain,
! [X0] :
( rR(X0,sK5,sK6)
| ~ ron(X0,vd1295)
| sK6 = X0
| sK5 = X0
| vd684 = vangle(sK5,X0,sK6)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1926,f567]) ).
fof(f1959,plain,
! [X0,X1] :
( ~ rR(vd1303,X0,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(X0,vd1303,X1) ),
inference(resolution,[],[f1104,f561]) ).
fof(f1962,plain,
! [X0,X1] :
( ~ rR(sK6,X0,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(X0,sK6,X1) ),
inference(resolution,[],[f1104,f565]) ).
fof(f1965,plain,
! [X0,X1] :
( rR(X0,X1,vd1300)
| ~ ron(X1,vd1295)
| ~ ron(X0,vd1295)
| vd1300 = X0
| X0 = X1
| vd684 = vangle(X1,X0,vd1300)
| ~ rpoint(vd1300)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f933,f1920]) ).
fof(f1966,plain,
! [X0,X1] :
( ~ ron(X1,vd1295)
| rR(X0,X1,vd1300)
| ~ ron(X0,vd1295)
| vd1300 = X0
| X0 = X1
| vd684 = vangle(X1,X0,vd1300)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1965,f564]) ).
fof(f1977,plain,
! [X0] :
( rR(X0,vd1303,sK4)
| ~ ron(X0,vd1297)
| sK4 = X0
| vd1303 = X0
| vd684 = vangle(vd1303,X0,sK4)
| ~ rpoint(vd1303)
| ~ rpoint(X0) ),
inference(resolution,[],[f1917,f932]) ).
fof(f1978,plain,
! [X0] :
( rR(X0,sK6,sK4)
| ~ ron(X0,vd1297)
| sK4 = X0
| sK6 = X0
| vd684 = vangle(sK6,X0,sK4)
| ~ rpoint(sK6)
| ~ rpoint(X0) ),
inference(resolution,[],[f1917,f935]) ).
fof(f1982,plain,
! [X0] :
( ~ ron(X0,vd1297)
| rR(X0,sK6,sK4)
| sK4 = X0
| sK6 = X0
| vd684 = vangle(sK6,X0,sK4)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1978,f565]) ).
fof(f1983,plain,
! [X0] :
( ~ ron(X0,vd1297)
| rR(X0,vd1303,sK4)
| sK4 = X0
| vd1303 = X0
| vd684 = vangle(vd1303,X0,sK4)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1977,f561]) ).
fof(f1987,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK4 = X1
| ~ rpoint(X0)
| sK4 = X0
| vangle(X0,X1,sK4) = vangle(sK4,X1,X0) ),
inference(resolution,[],[f1094,f569]) ).
fof(f1988,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK5 = X1
| ~ rpoint(X0)
| sK5 = X0
| vangle(X0,X1,sK5) = vangle(sK5,X1,X0) ),
inference(resolution,[],[f1094,f567]) ).
fof(f1989,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK6 = X1
| ~ rpoint(X0)
| sK6 = X0
| vangle(X0,X1,sK6) = vangle(sK6,X1,X0) ),
inference(resolution,[],[f1094,f565]) ).
fof(f2003,plain,
( vd1300 = sK6
| ~ spl55_20 ),
inference(avatar_component_clause,[],[f1816]) ).
fof(f2013,definition,
( spl55_39
<=> rR(sK5,sK6,sK6) ),
introduced(definition,[new_symbols(definition,[spl55_39])],[avatar_definition]) ).
fof(f2014,plain,
( rR(sK5,sK6,sK6)
| ~ spl55_39 ),
inference(avatar_component_clause,[],[f2013]) ).
fof(f2027,plain,
( rR(sK5,sK6,sK6)
| ~ spl55_20 ),
inference(superposition,[],[f1900,f2003]) ).
fof(f2031,plain,
( spl55_39
| ~ spl55_20 ),
inference(avatar_split_clause,[],[f2027,f1816,f2013]) ).
fof(f2070,definition,
( spl55_44
<=> vd1303 = sK5 ),
introduced(definition,[new_symbols(definition,[spl55_44])],[avatar_definition]) ).
fof(f2071,plain,
( vd1303 = sK5
| ~ spl55_44 ),
inference(avatar_component_clause,[],[f2070]) ).
fof(f2073,definition,
( spl55_45
<=> ron(vd1303,vd1295) ),
introduced(definition,[new_symbols(definition,[spl55_45])],[avatar_definition]) ).
fof(f2074,plain,
( ~ ron(vd1303,vd1295)
| spl55_45 ),
inference(avatar_component_clause,[],[f2073]) ).
fof(f2092,definition,
( spl55_46
<=> rR(sK5,vd1303,sK6) ),
introduced(definition,[new_symbols(definition,[spl55_46])],[avatar_definition]) ).
fof(f2093,plain,
( ~ rR(sK5,vd1303,sK6)
| spl55_46 ),
inference(avatar_component_clause,[],[f2092]) ).
fof(f2154,definition,
( spl55_53
<=> vd1300 = sK5 ),
introduced(definition,[new_symbols(definition,[spl55_53])],[avatar_definition]) ).
fof(f2155,plain,
( vd1300 = sK5
| ~ spl55_53 ),
inference(avatar_component_clause,[],[f2154]) ).
fof(f2201,plain,
! [X2,X0,X1] :
( ~ rR(X1,sK4,X0)
| ~ rR(X0,X1,X2)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X1,sK4,X2) ),
inference(resolution,[],[f1101,f569]) ).
fof(f2203,plain,
! [X2,X0,X1] :
( ~ rR(X1,sK6,X0)
| ~ rR(X0,X1,X2)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X1,sK6,X2) ),
inference(resolution,[],[f1101,f565]) ).
fof(f2214,definition,
( spl55_61
<=> vd1303 = sK4 ),
introduced(definition,[new_symbols(definition,[spl55_61])],[avatar_definition]) ).
fof(f2215,plain,
( vd1303 = sK4
| ~ spl55_61 ),
inference(avatar_component_clause,[],[f2214]) ).
fof(f2238,plain,
! [X0] :
( rR(X0,sK6,vd1303)
| ~ ron(X0,vd1297)
| vd1303 = X0
| sK6 = X0
| vd684 = vangle(sK6,X0,vd1303)
| ~ rpoint(sK6)
| ~ rpoint(X0) ),
inference(resolution,[],[f1919,f935]) ).
fof(f2239,plain,
! [X0] :
( rR(X0,sK4,vd1303)
| ~ ron(X0,vd1297)
| vd1303 = X0
| sK4 = X0
| vd684 = vangle(sK4,X0,vd1303)
| ~ rpoint(sK4)
| ~ rpoint(X0) ),
inference(resolution,[],[f1919,f934]) ).
fof(f2241,plain,
! [X0] :
( ~ ron(X0,vd1297)
| rR(X0,sK4,vd1303)
| vd1303 = X0
| sK4 = X0
| vd684 = vangle(sK4,X0,vd1303)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2239,f569]) ).
fof(f2242,plain,
! [X0] :
( ~ ron(X0,vd1297)
| rR(X0,sK6,vd1303)
| vd1303 = X0
| sK6 = X0
| vd684 = vangle(sK6,X0,vd1303)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2238,f565]) ).
fof(f2258,plain,
( rR(vd1303,sK6,sK4)
| vd1303 = sK4
| vd1303 = sK6
| vd684 = vangle(sK6,vd1303,sK4)
| ~ rpoint(vd1303) ),
inference(resolution,[],[f1982,f932]) ).
fof(f2261,plain,
( rR(vd1303,sK6,sK4)
| vd1303 = sK4
| vd684 = vangle(sK6,vd1303,sK4)
| ~ rpoint(vd1303) ),
inference(forward_subsumption_resolution,[],[f2258,f894]) ).
fof(f2262,plain,
( rR(vd1303,sK6,sK4)
| vd1303 = sK4
| vd684 = vangle(sK6,vd1303,sK4) ),
inference(forward_subsumption_resolution,[],[f2261,f561]) ).
fof(f2264,definition,
( spl55_65
<=> vd684 = vangle(sK6,vd1303,sK4) ),
introduced(definition,[new_symbols(definition,[spl55_65])],[avatar_definition]) ).
fof(f2265,plain,
( vd684 = vangle(sK6,vd1303,sK4)
| ~ spl55_65 ),
inference(avatar_component_clause,[],[f2264]) ).
fof(f2267,definition,
( spl55_66
<=> rR(vd1303,sK6,sK4) ),
introduced(definition,[new_symbols(definition,[spl55_66])],[avatar_definition]) ).
fof(f2268,plain,
( rR(vd1303,sK6,sK4)
| ~ spl55_66 ),
inference(avatar_component_clause,[],[f2267]) ).
fof(f2269,plain,
( spl55_65
| spl55_61
| spl55_66 ),
inference(avatar_split_clause,[],[f2262,f2267,f2214,f2264]) ).
fof(f2278,plain,
( rR(vd1303,vd1303,sK6)
| ~ spl55_61 ),
inference(superposition,[],[f1901,f2215]) ).
fof(f2300,plain,
( ~ rpoint(sK6)
| ~ rpoint(vd1303)
| ~ spl55_61 ),
inference(resolution,[],[f2278,f1739]) ).
fof(f2311,plain,
( ~ rpoint(vd1303)
| ~ spl55_61 ),
inference(forward_subsumption_resolution,[],[f2300,f565]) ).
fof(f2313,plain,
( $false
| ~ spl55_61 ),
inference(forward_subsumption_resolution,[],[f2311,f561]) ).
fof(f2314,plain,
~ spl55_61,
inference(avatar_contradiction_clause,[],[f2313]) ).
fof(f2316,plain,
( ! [X0] :
( vd684 != vd684
| ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK4
| vd1303 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ rpoint(vd1303) )
| ~ spl55_65 ),
inference(superposition,[],[f1049,f2265]) ).
fof(f2319,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK4
| vd1303 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ rpoint(vd1303) )
| ~ spl55_65 ),
inference(trivial_inequality_removal,[],[f2316]) ).
fof(f2329,definition,
( spl55_68
<=> rR(vd1303,sK4,sK6) ),
introduced(definition,[new_symbols(definition,[spl55_68])],[avatar_definition]) ).
fof(f2330,plain,
( rR(vd1303,sK4,sK6)
| ~ spl55_68 ),
inference(avatar_component_clause,[],[f2329]) ).
fof(f2371,plain,
! [X0] :
( rR(X0,sK5,vd1300)
| ~ ron(X0,vd1295)
| vd1300 = X0
| sK5 = X0
| vd684 = vangle(sK5,X0,vd1300)
| ~ rpoint(sK5)
| ~ rpoint(X0) ),
inference(resolution,[],[f1966,f927]) ).
fof(f2375,plain,
! [X0] :
( ~ ron(X0,vd1295)
| rR(X0,sK5,vd1300)
| vd1300 = X0
| sK5 = X0
| vd684 = vangle(sK5,X0,vd1300)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2371,f567]) ).
fof(f2412,plain,
( ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ spl55_39 ),
inference(resolution,[],[f2014,f1740]) ).
fof(f2423,plain,
( ~ rpoint(sK5)
| ~ spl55_39 ),
inference(forward_subsumption_resolution,[],[f2412,f565]) ).
fof(f2425,plain,
( $false
| ~ spl55_39 ),
inference(forward_subsumption_resolution,[],[f2423,f567]) ).
fof(f2426,plain,
~ spl55_39,
inference(avatar_contradiction_clause,[],[f2425]) ).
fof(f2623,plain,
! [X0,X1] :
( rinside(X0,sK14(X0,X1))
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f739,f1220]) ).
fof(f2722,plain,
! [X0] :
( ~ rR(vd1300,sK5,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1300)
| ~ rpoint(sK5)
| rR(sK5,sK6,X0) ),
inference(resolution,[],[f2203,f880]) ).
fof(f2724,plain,
! [X0] :
( ~ rR(vd1300,sK5,X0)
| ~ rpoint(X0)
| ~ rpoint(sK5)
| rR(sK5,sK6,X0) ),
inference(forward_subsumption_resolution,[],[f2722,f564]) ).
fof(f2729,plain,
! [X0] :
( ~ rR(vd1300,sK5,X0)
| ~ rpoint(X0)
| rR(sK5,sK6,X0) ),
inference(forward_subsumption_resolution,[],[f2724,f567]) ).
fof(f2753,plain,
! [X2,X3,X0,X1,X4] :
( ~ rcenter(X0,X3)
| ~ ron(X1,X3)
| ~ ron(X2,sK14(X0,X4))
| vf(X0,X2) != vf(X0,X1)
| sK14(X0,X4) = X3
| ~ rpoint(X1)
| ~ rpoint(X2)
| X0 = X4
| ~ rpoint(X4)
| ~ rpoint(X0) ),
inference(resolution,[],[f1175,f1220]) ).
fof(f2796,plain,
! [X2,X0,X1] :
( ~ ron(X0,vd1297)
| ~ ron(X1,vd1297)
| ~ rR(X0,X1,X2)
| ron(X2,vd1297)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f1249,f685]) ).
fof(f2797,plain,
! [X2,X0,X1] :
( ~ ron(X0,vd1295)
| ~ ron(X1,vd1295)
| ~ rR(X0,X1,X2)
| ron(X2,vd1295)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f1249,f687]) ).
fof(f2907,plain,
! [X0] :
( sK5 = sK6
| ~ rpoint(X0)
| sK6 = X0
| vangle(X0,sK5,sK6) = vangle(sK6,sK5,X0) ),
inference(resolution,[],[f1989,f567]) ).
fof(f2909,plain,
! [X0] :
( ~ rpoint(X0)
| sK6 = X0
| vangle(X0,sK5,sK6) = vangle(sK6,sK5,X0) ),
inference(forward_subsumption_resolution,[],[f2907,f928]) ).
fof(f2965,definition,
( spl55_84
<=> vd1300 = sK4 ),
introduced(definition,[new_symbols(definition,[spl55_84])],[avatar_definition]) ).
fof(f2966,plain,
( vd1300 = sK4
| ~ spl55_84 ),
inference(avatar_component_clause,[],[f2965]) ).
fof(f3111,plain,
( ron(vd1300,vd1297)
| ~ spl55_84 ),
inference(superposition,[],[f934,f2966]) ).
fof(f3214,plain,
( vd1303 = sK6
| vangle(sK6,sK5,vd1303) = vangle(vd1303,sK5,sK6) ),
inference(resolution,[],[f2909,f561]) ).
fof(f3220,plain,
vangle(sK6,sK5,vd1303) = vangle(vd1303,sK5,sK6),
inference(forward_subsumption_resolution,[],[f3214,f894]) ).
fof(f3234,plain,
( ~ rpoint(sK6)
| rR(sK5,sK6,sK6)
| ~ ron(vd1300,vd1295)
| vd1300 = sK6
| vd1300 = sK5
| vd684 = vangle(sK5,vd1300,sK6)
| ~ rpoint(vd1300) ),
inference(resolution,[],[f2729,f1930]) ).
fof(f3236,plain,
( rR(sK5,sK6,sK6)
| ~ ron(vd1300,vd1295)
| vd1300 = sK6
| vd1300 = sK5
| vd684 = vangle(sK5,vd1300,sK6)
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f3234,f565]) ).
fof(f3237,plain,
( rR(sK5,sK6,sK6)
| vd1300 = sK6
| vd1300 = sK5
| vd684 = vangle(sK5,vd1300,sK6)
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f3236,f933]) ).
fof(f3238,plain,
( rR(sK5,sK6,sK6)
| vd1300 = sK5
| vd684 = vangle(sK5,vd1300,sK6)
| ~ rpoint(vd1300)
| spl55_20 ),
inference(forward_subsumption_resolution,[],[f3237,f1817]) ).
fof(f3239,plain,
( rR(sK5,sK6,sK6)
| vd1300 = sK5
| vd684 = vangle(sK5,vd1300,sK6)
| spl55_20 ),
inference(forward_subsumption_resolution,[],[f3238,f564]) ).
fof(f3309,plain,
vangle(sK6,sK4,vd1329) = vangle(vd1303,sK5,sK6),
inference(forward_demodulation,[],[f3220,f868]) ).
fof(f3311,definition,
( spl55_94
<=> vd684 = vangle(sK5,vd1300,sK6) ),
introduced(definition,[new_symbols(definition,[spl55_94])],[avatar_definition]) ).
fof(f3312,plain,
( vd684 = vangle(sK5,vd1300,sK6)
| ~ spl55_94 ),
inference(avatar_component_clause,[],[f3311]) ).
fof(f3313,plain,
( spl55_94
| spl55_53
| spl55_39
| spl55_20 ),
inference(avatar_split_clause,[],[f3239,f1816,f2013,f2154,f3311]) ).
fof(f3336,plain,
( rR(vd1300,vd1300,sK6)
| ~ spl55_53 ),
inference(superposition,[],[f1900,f2155]) ).
fof(f3588,plain,
vd684 = vplus(vd684,vd684),
inference(resolution,[],[f1228,f692]) ).
fof(f3665,plain,
! [X0] :
( sK5 = sK6
| ~ rpoint(X0)
| sK5 = X0
| vangle(sK5,sK6,X0) = vangle(X0,sK6,sK5) ),
inference(resolution,[],[f1988,f565]) ).
fof(f3666,plain,
! [X0] :
( ~ rpoint(X0)
| sK5 = X0
| vangle(sK5,sK6,X0) = vangle(X0,sK6,sK5) ),
inference(forward_subsumption_resolution,[],[f3665,f928]) ).
fof(f3686,plain,
! [X0] :
( sK4 = sK5
| ~ rpoint(X0)
| sK4 = X0
| vangle(X0,sK5,sK4) = vangle(sK4,sK5,X0) ),
inference(resolution,[],[f1987,f567]) ).
fof(f3689,plain,
! [X0] :
( ~ rpoint(X0)
| sK4 = X0
| vangle(X0,sK5,sK4) = vangle(sK4,sK5,X0) ),
inference(forward_subsumption_resolution,[],[f3686,f882]) ).
fof(f3981,plain,
( rR(sK6,sK4,vd1303)
| vd1303 = sK6
| sK4 = sK6
| vd684 = vangle(sK4,sK6,vd1303)
| ~ rpoint(sK6) ),
inference(resolution,[],[f2241,f935]) ).
fof(f3983,plain,
( vd1303 = sK6
| sK4 = sK6
| vd684 = vangle(sK4,sK6,vd1303)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f3981,f877]) ).
fof(f3984,plain,
( sK4 = sK6
| vd684 = vangle(sK4,sK6,vd1303)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f3983,f894]) ).
fof(f3985,plain,
( vd684 = vangle(sK4,sK6,vd1303)
| ~ rpoint(sK6)
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f3984,f1822]) ).
fof(f3986,plain,
( vd684 = vangle(sK4,sK6,vd1303)
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f3985,f565]) ).
fof(f4262,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,sK14(X0,X3))
| vf(X0,X2) != vf(X0,X1)
| ~ rpoint(X2)
| ron(X1,sK14(X0,X3))
| ~ rpoint(X1)
| X0 = X3
| ~ rpoint(X3)
| ~ rpoint(X0) ),
inference(resolution,[],[f1119,f1220]) ).
fof(f4263,plain,
! [X2,X0,X1] :
( vf(X0,X2) != vf(X0,X1)
| ~ rpoint(X1)
| ron(X2,sK14(X0,X1))
| ~ rpoint(X2)
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f4262,f1218]) ).
fof(f4264,plain,
! [X2,X0,X1] :
( ron(X2,sK14(X0,X1))
| ~ rpoint(X1)
| vf(X0,X2) != vf(X0,X1)
| ~ rpoint(X2)
| X0 = X1
| ~ rpoint(X0) ),
inference(duplicate_literal_removal,[],[f4263]) ).
fof(f4339,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ rline(X5)
| ~ rpoint(X0)
| ~ rpoint(X1)
| X2 = X3
| ~ ron(X2,sK14(X1,X0))
| ~ ron(X3,sK14(X1,X0))
| ~ rinside(X4,sK14(X1,X0))
| ~ ron(X2,X5)
| ~ ron(X3,X5)
| ~ ron(X4,X5)
| rR(X4,X3,X2)
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(resolution,[],[f1222,f1346]) ).
fof(f4498,plain,
( rR(sK6,sK5,vd1300)
| vd1300 = sK6
| sK5 = sK6
| vd684 = vangle(sK5,sK6,vd1300)
| ~ rpoint(sK6) ),
inference(resolution,[],[f2375,f938]) ).
fof(f4499,plain,
( rR(sK6,sK5,vd1300)
| sK5 = sK6
| vd684 = vangle(sK5,sK6,vd1300)
| ~ rpoint(sK6)
| spl55_20 ),
inference(forward_subsumption_resolution,[],[f4498,f1817]) ).
fof(f4502,plain,
( rR(sK6,sK5,vd1300)
| vd684 = vangle(sK5,sK6,vd1300)
| ~ rpoint(sK6)
| spl55_20 ),
inference(forward_subsumption_resolution,[],[f4499,f928]) ).
fof(f4505,plain,
( rR(sK6,sK5,vd1300)
| vd684 = vangle(sK5,sK6,vd1300)
| spl55_20 ),
inference(forward_subsumption_resolution,[],[f4502,f565]) ).
fof(f4526,plain,
( ~ rpoint(sK6)
| ~ rpoint(vd1300)
| ~ spl55_53 ),
inference(resolution,[],[f3336,f1739]) ).
fof(f4537,plain,
( ~ rpoint(vd1300)
| ~ spl55_53 ),
inference(forward_subsumption_resolution,[],[f4526,f565]) ).
fof(f4539,plain,
( $false
| ~ spl55_53 ),
inference(forward_subsumption_resolution,[],[f4537,f564]) ).
fof(f4540,plain,
~ spl55_53,
inference(avatar_contradiction_clause,[],[f4539]) ).
fof(f4595,definition,
( spl55_126
<=> vd684 = vangle(sK5,sK6,vd1300) ),
introduced(definition,[new_symbols(definition,[spl55_126])],[avatar_definition]) ).
fof(f4596,plain,
( vd684 = vangle(sK5,sK6,vd1300)
| ~ spl55_126 ),
inference(avatar_component_clause,[],[f4595]) ).
fof(f4597,plain,
( rR(sK6,sK5,vd1300)
| ~ spl55_22 ),
inference(avatar_component_clause,[],[f1827]) ).
fof(f4598,plain,
( spl55_126
| spl55_22
| spl55_20 ),
inference(avatar_split_clause,[],[f4505,f1816,f1827,f4595]) ).
fof(f4652,definition,
( spl55_129
<=> rR(sK5,sK6,sK4) ),
introduced(definition,[new_symbols(definition,[spl55_129])],[avatar_definition]) ).
fof(f4653,plain,
( rR(sK5,sK6,sK4)
| ~ spl55_129 ),
inference(avatar_component_clause,[],[f4652]) ).
fof(f4655,definition,
( spl55_130
<=> vd684 = vangle(sK6,sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl55_130])],[avatar_definition]) ).
fof(f4656,plain,
( vd684 = vangle(sK6,sK5,sK4)
| ~ spl55_130 ),
inference(avatar_component_clause,[],[f4655]) ).
fof(f5001,plain,
( ! [X0] :
( vd684 != vd684
| ~ rR(vd1300,sK5,sK6)
| ~ ron(sK5,X0)
| ~ ron(vd1300,X0)
| vd1300 = sK6
| vd1300 = sK5
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(vd1300) )
| ~ spl55_94 ),
inference(superposition,[],[f1045,f3312]) ).
fof(f5002,plain,
( ! [X0] :
( ~ rR(vd1300,sK5,sK6)
| ~ ron(sK5,X0)
| ~ ron(vd1300,X0)
| vd1300 = sK6
| vd1300 = sK5
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(vd1300) )
| ~ spl55_94 ),
inference(trivial_inequality_removal,[],[f5001]) ).
fof(f5005,plain,
( vd1300 = sK5
| vangle(vd1300,sK6,sK5) = vangle(sK5,sK6,vd1300) ),
inference(resolution,[],[f3666,f564]) ).
fof(f5017,plain,
( vd684 = vangle(vd1300,sK6,sK5)
| vd1300 = sK5
| ~ spl55_126 ),
inference(forward_demodulation,[],[f5005,f4596]) ).
fof(f5024,definition,
( spl55_152
<=> vd684 = vangle(vd1300,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl55_152])],[avatar_definition]) ).
fof(f5025,plain,
( vd684 = vangle(vd1300,sK6,sK5)
| ~ spl55_152 ),
inference(avatar_component_clause,[],[f5024]) ).
fof(f5026,plain,
( spl55_53
| spl55_152
| ~ spl55_126 ),
inference(avatar_split_clause,[],[f5017,f4595,f5024,f2154]) ).
fof(f5060,definition,
( spl55_153
<=> rR(sK6,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl55_153])],[avatar_definition]) ).
fof(f5061,plain,
( rR(sK6,sK4,sK5)
| ~ spl55_153 ),
inference(avatar_component_clause,[],[f5060]) ).
fof(f5270,plain,
( vd1303 = sK4
| vangle(sK4,sK5,vd1303) = vangle(vd1303,sK5,sK4) ),
inference(resolution,[],[f3689,f561]) ).
fof(f8327,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X0,sK14(X1,X2))
| ~ ron(X3,sK14(X1,X4))
| vf(X1,X0) != vf(X1,X3)
| sK14(X1,X2) = sK14(X1,X4)
| ~ rpoint(X0)
| ~ rpoint(X3)
| X1 = X4
| ~ rpoint(X4)
| ~ rpoint(X1)
| X1 = X2
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(resolution,[],[f2753,f1220]) ).
fof(f8328,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X0,sK14(X1,X2))
| ~ ron(X3,sK14(X1,X4))
| vf(X1,X0) != vf(X1,X3)
| sK14(X1,X2) = sK14(X1,X4)
| ~ rpoint(X0)
| ~ rpoint(X3)
| X1 = X4
| ~ rpoint(X4)
| ~ rpoint(X1)
| X1 = X2
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f8327]) ).
fof(f8485,plain,
! [X0,X1] :
( ~ ron(X0,vd1297)
| ~ rR(sK6,X0,X1)
| ron(X1,vd1297)
| ~ rpoint(X1)
| ~ rpoint(sK6)
| ~ rpoint(X0) ),
inference(resolution,[],[f2796,f935]) ).
fof(f8488,plain,
! [X0,X1] :
( ~ rR(sK6,X0,X1)
| ~ ron(X0,vd1297)
| ron(X1,vd1297)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f8485,f565]) ).
fof(f8492,plain,
! [X0,X1] :
( ~ ron(X0,vd1295)
| ~ rR(vd1300,X0,X1)
| ron(X1,vd1295)
| ~ rpoint(X1)
| ~ rpoint(vd1300)
| ~ rpoint(X0) ),
inference(resolution,[],[f2797,f933]) ).
fof(f8494,plain,
! [X0,X1] :
( ~ ron(X0,vd1295)
| ~ rR(sK5,X0,X1)
| ron(X1,vd1295)
| ~ rpoint(X1)
| ~ rpoint(sK5)
| ~ rpoint(X0) ),
inference(resolution,[],[f2797,f927]) ).
fof(f8497,plain,
! [X0,X1] :
( ~ ron(X0,vd1295)
| ~ rR(sK5,X0,X1)
| ron(X1,vd1295)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f8494,f567]) ).
fof(f8499,plain,
! [X0,X1] :
( ~ rR(vd1300,X0,X1)
| ~ ron(X0,vd1295)
| ron(X1,vd1295)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f8492,f564]) ).
fof(f13373,definition,
( spl55_442
<=> vd684 = vangle(sK6,sK4,vd1329) ),
introduced(definition,[new_symbols(definition,[spl55_442])],[avatar_definition]) ).
fof(f13374,plain,
( vd684 = vangle(sK6,sK4,vd1329)
| ~ spl55_442 ),
inference(avatar_component_clause,[],[f13373]) ).
fof(f15371,plain,
! [X2,X3,X0,X1] :
( ~ ron(X0,sK14(X1,X2))
| vf(X1,X0) != vf(X1,X3)
| sK14(X1,X2) = sK14(X1,X3)
| ~ rpoint(X3)
| ~ rpoint(X0)
| X1 = X2
| ~ rpoint(X2)
| ~ rpoint(X1)
| X1 = X3
| ~ rpoint(X3)
| X1 = X3
| ~ rpoint(X3)
| ~ rpoint(X1) ),
inference(resolution,[],[f8328,f1218]) ).
fof(f15374,plain,
! [X2,X3,X0,X1] :
( ~ ron(X0,sK14(X1,X2))
| vf(X1,X0) != vf(X1,X3)
| sK14(X1,X2) = sK14(X1,X3)
| ~ rpoint(X3)
| ~ rpoint(X0)
| X1 = X2
| ~ rpoint(X2)
| ~ rpoint(X1)
| X1 = X3 ),
inference(duplicate_literal_removal,[],[f15371]) ).
fof(f15375,plain,
! [X2,X0,X1] :
( vf(X0,X2) != vf(X0,X1)
| sK14(X0,X1) = sK14(X0,X2)
| ~ rpoint(X2)
| ~ rpoint(X1)
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X2
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f15374,f1218]) ).
fof(f15378,plain,
! [X2,X0,X1] :
( ~ rpoint(X0)
| sK14(X0,X1) = sK14(X0,X2)
| ~ rpoint(X2)
| ~ rpoint(X1)
| X0 = X1
| vf(X0,X2) != vf(X0,X1)
| X0 = X2 ),
inference(duplicate_literal_removal,[],[f15375]) ).
fof(f15392,plain,
! [X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| sK14(sK6,X0) = sK14(sK6,X1)
| sK6 = X0
| vf(sK6,X0) != vf(sK6,X1)
| sK6 = X1 ),
inference(resolution,[],[f15378,f565]) ).
fof(f16296,plain,
! [X0] :
( ~ rpoint(X0)
| vf(sK6,X0) = sK11(sK6,X0) ),
inference(resolution,[],[f1177,f565]) ).
fof(f16370,plain,
vf(sK6,sK4) = sK11(sK6,sK4),
inference(resolution,[],[f16296,f569]) ).
fof(f16747,plain,
! [X0] :
( ~ rR(sK5,sK6,X0)
| ron(X0,vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(resolution,[],[f8497,f938]) ).
fof(f16748,plain,
! [X0] :
( ~ rR(sK5,sK6,X0)
| ron(X0,vd1295)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f16747,f565]) ).
fof(f18863,definition,
( spl55_574
<=> rR(sK6,sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl55_574])],[avatar_definition]) ).
fof(f18864,plain,
( rR(sK6,sK5,sK4)
| ~ spl55_574 ),
inference(avatar_component_clause,[],[f18863]) ).
fof(f19076,plain,
( ~ rpoint(sK4)
| ~ rpoint(sK5)
| ~ rR(sK5,sK6,sK4)
| ~ spl55_574 ),
inference(resolution,[],[f18864,f1962]) ).
fof(f19105,plain,
( ~ rpoint(sK5)
| ~ rR(sK5,sK6,sK4)
| ~ spl55_574 ),
inference(forward_subsumption_resolution,[],[f19076,f569]) ).
fof(f19118,plain,
( ~ rR(sK5,sK6,sK4)
| ~ spl55_574 ),
inference(forward_subsumption_resolution,[],[f19105,f567]) ).
fof(f19127,plain,
( $false
| ~ spl55_129
| ~ spl55_574 ),
inference(forward_subsumption_resolution,[],[f19118,f4653]) ).
fof(f19128,plain,
( ~ spl55_129
| ~ spl55_574 ),
inference(avatar_contradiction_clause,[],[f19127]) ).
fof(f19927,plain,
( ~ rpoint(vd1300)
| ~ rpoint(sK5)
| ~ rR(sK5,sK6,vd1300)
| ~ spl55_22 ),
inference(resolution,[],[f4597,f1962]) ).
fof(f19962,plain,
( ~ rpoint(sK5)
| ~ rR(sK5,sK6,vd1300)
| ~ spl55_22 ),
inference(forward_subsumption_resolution,[],[f19927,f564]) ).
fof(f19973,plain,
( ~ rR(sK5,sK6,vd1300)
| ~ spl55_22 ),
inference(forward_subsumption_resolution,[],[f19962,f567]) ).
fof(f19985,plain,
( $false
| ~ spl55_22 ),
inference(forward_subsumption_resolution,[],[f19973,f880]) ).
fof(f19986,plain,
~ spl55_22,
inference(avatar_contradiction_clause,[],[f19985]) ).
fof(f19995,plain,
( ! [X0] :
( vd684 != vd684
| ron(vd1300,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| vd1300 = sK6
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(vd1300)
| ~ rpoint(sK5)
| ~ rpoint(sK6) )
| ~ spl55_126 ),
inference(superposition,[],[f1049,f4596]) ).
fof(f19998,plain,
( ! [X0] :
( ron(vd1300,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| vd1300 = sK6
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(vd1300)
| ~ rpoint(sK5)
| ~ rpoint(sK6) )
| ~ spl55_126 ),
inference(trivial_inequality_removal,[],[f19995]) ).
fof(f20096,plain,
( ! [X0] :
( vd684 != vd684
| ron(sK5,X0)
| ~ ron(vd1300,X0)
| ~ ron(sK6,X0)
| sK5 = sK6
| vd1300 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1300)
| ~ rpoint(sK6) )
| ~ spl55_152 ),
inference(superposition,[],[f1049,f5025]) ).
fof(f20099,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ ron(vd1300,X0)
| ~ ron(sK6,X0)
| sK5 = sK6
| vd1300 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1300)
| ~ rpoint(sK6) )
| ~ spl55_152 ),
inference(trivial_inequality_removal,[],[f20096]) ).
fof(f22552,plain,
( ron(sK4,vd1295)
| ~ rpoint(sK4)
| ~ spl55_129 ),
inference(resolution,[],[f4653,f16748]) ).
fof(f26187,plain,
! [X0] :
( ~ rpoint(X0)
| sK14(sK6,X0) = sK14(sK6,sK5)
| sK5 = sK6
| vf(sK6,sK5) != vf(sK6,X0)
| sK6 = X0 ),
inference(resolution,[],[f15392,f567]) ).
fof(f26189,plain,
! [X0] :
( ~ rpoint(X0)
| sK14(sK6,X0) = sK14(sK6,sK5)
| vf(sK6,sK5) != vf(sK6,X0)
| sK6 = X0 ),
inference(forward_subsumption_resolution,[],[f26187,f928]) ).
fof(f26198,plain,
! [X0] :
( vf(sK6,sK4) != vf(sK6,X0)
| ~ rpoint(X0)
| sK14(sK6,X0) = sK14(sK6,sK5)
| sK6 = X0 ),
inference(forward_demodulation,[],[f26189,f881]) ).
fof(f26207,plain,
! [X0] :
( vf(sK6,X0) != sK11(sK6,sK4)
| ~ rpoint(X0)
| sK14(sK6,X0) = sK14(sK6,sK5)
| sK6 = X0 ),
inference(forward_demodulation,[],[f26198,f16370]) ).
fof(f29934,plain,
( sK11(sK6,sK4) != sK11(sK6,sK4)
| ~ rpoint(sK4)
| sK14(sK6,sK4) = sK14(sK6,sK5)
| sK4 = sK6 ),
inference(superposition,[],[f26207,f16370]) ).
fof(f29935,plain,
( ~ rpoint(sK4)
| sK14(sK6,sK4) = sK14(sK6,sK5)
| sK4 = sK6 ),
inference(trivial_inequality_removal,[],[f29934]) ).
fof(f29936,plain,
( sK14(sK6,sK4) = sK14(sK6,sK5)
| sK4 = sK6 ),
inference(forward_subsumption_resolution,[],[f29935,f569]) ).
fof(f29940,plain,
( sK14(sK6,sK4) = sK14(sK6,sK5)
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f29936,f1822]) ).
fof(f29950,plain,
( ron(sK5,sK14(sK6,sK4))
| sK5 = sK6
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| spl55_21 ),
inference(superposition,[],[f1218,f29940]) ).
fof(f29953,plain,
( rinside(sK6,sK14(sK6,sK4))
| sK5 = sK6
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| spl55_21 ),
inference(superposition,[],[f2623,f29940]) ).
fof(f29955,plain,
( ! [X0] :
( ron(X0,sK14(sK6,sK4))
| ~ rpoint(sK5)
| vf(sK6,sK5) != vf(sK6,X0)
| ~ rpoint(X0)
| sK5 = sK6
| ~ rpoint(sK6) )
| spl55_21 ),
inference(superposition,[],[f4264,f29940]) ).
fof(f29972,plain,
( ! [X0] :
( ron(X0,sK14(sK6,sK4))
| vf(sK6,sK5) != vf(sK6,X0)
| ~ rpoint(X0)
| sK5 = sK6
| ~ rpoint(sK6) )
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f29955,f567]) ).
fof(f29974,plain,
( rinside(sK6,sK14(sK6,sK4))
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f29953,f928]) ).
fof(f29977,plain,
( ron(sK5,sK14(sK6,sK4))
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f29950,f928]) ).
fof(f29986,plain,
( ! [X0] :
( ron(X0,sK14(sK6,sK4))
| vf(sK6,sK5) != vf(sK6,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6) )
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f29972,f928]) ).
fof(f29988,plain,
( rinside(sK6,sK14(sK6,sK4))
| ~ rpoint(sK6)
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f29974,f567]) ).
fof(f29991,plain,
( ron(sK5,sK14(sK6,sK4))
| ~ rpoint(sK6)
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f29977,f567]) ).
fof(f30000,plain,
( ! [X0] :
( ron(X0,sK14(sK6,sK4))
| vf(sK6,sK5) != vf(sK6,X0)
| ~ rpoint(X0) )
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f29986,f565]) ).
fof(f30002,plain,
( rinside(sK6,sK14(sK6,sK4))
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f29988,f565]) ).
fof(f30005,plain,
( ron(sK5,sK14(sK6,sK4))
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f29991,f565]) ).
fof(f30009,plain,
( ! [X0] :
( vf(sK6,sK4) != vf(sK6,X0)
| ron(X0,sK14(sK6,sK4))
| ~ rpoint(X0) )
| spl55_21 ),
inference(forward_demodulation,[],[f30000,f881]) ).
fof(f30014,plain,
( ! [X0] :
( vf(sK6,X0) != sK11(sK6,sK4)
| ron(X0,sK14(sK6,sK4))
| ~ rpoint(X0) )
| spl55_21 ),
inference(forward_demodulation,[],[f30009,f16370]) ).
fof(f39660,plain,
( sK11(sK6,sK4) != sK11(sK6,sK4)
| ron(sK4,sK14(sK6,sK4))
| ~ rpoint(sK4)
| spl55_21 ),
inference(superposition,[],[f30014,f16370]) ).
fof(f39664,plain,
( ron(sK4,sK14(sK6,sK4))
| ~ rpoint(sK4)
| spl55_21 ),
inference(trivial_inequality_removal,[],[f39660]) ).
fof(f39665,plain,
( ron(sK4,sK14(sK6,sK4))
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f39664,f569]) ).
fof(f47626,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK4
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ rpoint(vd1303) )
| ~ spl55_65 ),
inference(forward_subsumption_resolution,[],[f2319,f894]) ).
fof(f47647,plain,
( ! [X0] :
( ~ rR(vd1300,sK5,sK6)
| ~ ron(sK5,X0)
| ~ ron(vd1300,X0)
| vd1300 = sK5
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(vd1300) )
| spl55_20
| ~ spl55_94 ),
inference(forward_subsumption_resolution,[],[f5002,f1817]) ).
fof(f47699,plain,
( ! [X0] :
( ron(vd1300,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(vd1300)
| ~ rpoint(sK5)
| ~ rpoint(sK6) )
| spl55_20
| ~ spl55_126 ),
inference(forward_subsumption_resolution,[],[f19998,f1817]) ).
fof(f47700,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ ron(vd1300,X0)
| ~ ron(sK6,X0)
| vd1300 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1300)
| ~ rpoint(sK6) )
| ~ spl55_152 ),
inference(forward_subsumption_resolution,[],[f20099,f928]) ).
fof(f47753,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK4
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(vd1303) )
| ~ spl55_65 ),
inference(forward_subsumption_resolution,[],[f47626,f569]) ).
fof(f47774,plain,
( ! [X0] :
( ~ rR(vd1300,sK5,sK6)
| ~ ron(sK5,X0)
| ~ ron(vd1300,X0)
| vd1300 = sK5
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1300) )
| spl55_20
| ~ spl55_94 ),
inference(forward_subsumption_resolution,[],[f47647,f565]) ).
fof(f47826,plain,
( ! [X0] :
( ron(vd1300,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(vd1300)
| ~ rpoint(sK5)
| ~ rpoint(sK6) )
| spl55_20
| ~ spl55_126 ),
inference(forward_subsumption_resolution,[],[f47699,f928]) ).
fof(f47827,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ ron(vd1300,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(vd1300)
| ~ rpoint(sK6) )
| spl55_20
| ~ spl55_152 ),
inference(forward_subsumption_resolution,[],[f47700,f1817]) ).
fof(f47880,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK4
| ~ rline(X0)
| ~ rpoint(vd1303) )
| ~ spl55_65 ),
inference(forward_subsumption_resolution,[],[f47753,f565]) ).
fof(f47901,plain,
( ! [X0] :
( ~ rR(vd1300,sK5,sK6)
| ~ ron(sK5,X0)
| ~ ron(vd1300,X0)
| vd1300 = sK5
| ~ rline(X0)
| ~ rpoint(vd1300) )
| spl55_20
| ~ spl55_94 ),
inference(forward_subsumption_resolution,[],[f47774,f567]) ).
fof(f47953,plain,
( ! [X0] :
( ron(vd1300,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6) )
| spl55_20
| ~ spl55_126 ),
inference(forward_subsumption_resolution,[],[f47826,f564]) ).
fof(f47954,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ ron(vd1300,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(vd1300)
| ~ rpoint(sK6) )
| spl55_20
| ~ spl55_152 ),
inference(forward_subsumption_resolution,[],[f47827,f567]) ).
fof(f48007,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1303,X0)
| vd1303 = sK4
| ~ rline(X0) )
| ~ spl55_65 ),
inference(forward_subsumption_resolution,[],[f47880,f561]) ).
fof(f48026,definition,
( spl55_1878
<=> ! [X0] :
( ~ ron(sK5,X0)
| ~ rline(X0)
| ~ ron(vd1300,X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_1878])],[avatar_definition]) ).
fof(f48027,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ rline(X0)
| ~ ron(vd1300,X0) )
| ~ spl55_1878 ),
inference(avatar_component_clause,[],[f48026]) ).
fof(f48035,plain,
( ! [X0] :
( ~ rR(vd1300,sK5,sK6)
| ~ ron(sK5,X0)
| ~ ron(vd1300,X0)
| vd1300 = sK5
| ~ rline(X0) )
| spl55_20
| ~ spl55_94 ),
inference(forward_subsumption_resolution,[],[f47901,f564]) ).
fof(f48102,plain,
( ! [X0] :
( ron(vd1300,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK6) )
| spl55_20
| ~ spl55_126 ),
inference(forward_subsumption_resolution,[],[f47953,f567]) ).
fof(f48103,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ ron(vd1300,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK6) )
| spl55_20
| ~ spl55_152 ),
inference(forward_subsumption_resolution,[],[f47954,f564]) ).
fof(f48205,definition,
( spl55_1894
<=> ! [X0] :
( ron(sK5,X0)
| ~ rline(X0)
| ~ ron(vd1300,X0)
| ~ ron(sK6,X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_1894])],[avatar_definition]) ).
fof(f48206,plain,
( ! [X0] :
( ~ rline(X0)
| ron(sK5,X0)
| ~ ron(vd1300,X0)
| ~ ron(sK6,X0) )
| ~ spl55_1894 ),
inference(avatar_component_clause,[],[f48205]) ).
fof(f48220,definition,
( spl55_1896
<=> rR(vd1300,sK5,sK6) ),
introduced(definition,[new_symbols(definition,[spl55_1896])],[avatar_definition]) ).
fof(f48221,plain,
( ~ rR(vd1300,sK5,sK6)
| spl55_1896 ),
inference(avatar_component_clause,[],[f48220]) ).
fof(f48222,plain,
( spl55_53
| spl55_1878
| ~ spl55_1896
| spl55_20
| ~ spl55_94 ),
inference(avatar_split_clause,[],[f48035,f3311,f1816,f48220,f48026,f2154]) ).
fof(f48270,definition,
( spl55_1902
<=> rR(vd1300,sK6,sK4) ),
introduced(definition,[new_symbols(definition,[spl55_1902])],[avatar_definition]) ).
fof(f48274,definition,
( spl55_1903
<=> ! [X0] :
( ron(sK4,X0)
| ~ rline(X0)
| ~ ron(vd1300,X0)
| ~ ron(sK6,X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_1903])],[avatar_definition]) ).
fof(f48275,plain,
( ! [X0] :
( ~ rline(X0)
| ron(sK4,X0)
| ~ ron(vd1300,X0)
| ~ ron(sK6,X0) )
| ~ spl55_1903 ),
inference(avatar_component_clause,[],[f48274]) ).
fof(f48308,plain,
( ! [X0] :
( ron(vd1300,X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ rline(X0) )
| spl55_20
| ~ spl55_126 ),
inference(forward_subsumption_resolution,[],[f48102,f565]) ).
fof(f48309,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ ron(vd1300,X0)
| ~ ron(sK6,X0)
| ~ rline(X0) )
| spl55_20
| ~ spl55_152 ),
inference(forward_subsumption_resolution,[],[f48103,f565]) ).
fof(f48377,plain,
( vd684 != vangle(sK6,sK5,sK4)
| spl55_130 ),
inference(avatar_component_clause,[],[f4655]) ).
fof(f48394,definition,
( spl55_1918
<=> ! [X0] :
( ron(vd1300,X0)
| ~ rline(X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_1918])],[avatar_definition]) ).
fof(f48395,plain,
( ! [X0] :
( ron(vd1300,X0)
| ~ rline(X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0) )
| ~ spl55_1918 ),
inference(avatar_component_clause,[],[f48394]) ).
fof(f48405,definition,
( spl55_1919
<=> ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_1919])],[avatar_definition]) ).
fof(f48406,plain,
( ! [X0] :
( ~ rline(X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0) )
| ~ spl55_1919 ),
inference(avatar_component_clause,[],[f48405]) ).
fof(f48423,plain,
( spl55_1918
| spl55_20
| ~ spl55_126 ),
inference(avatar_split_clause,[],[f48308,f4595,f1816,f48394]) ).
fof(f48424,plain,
( spl55_1894
| spl55_20
| ~ spl55_152 ),
inference(avatar_split_clause,[],[f48309,f5024,f1816,f48205]) ).
fof(f48425,plain,
( ~ rR(sK6,sK4,sK5)
| spl55_153 ),
inference(avatar_component_clause,[],[f5060]) ).
fof(f48472,plain,
( ~ rR(sK6,sK5,sK4)
| spl55_574 ),
inference(avatar_component_clause,[],[f18863]) ).
fof(f48496,plain,
( ! [X0] :
( ~ rline(X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0) )
| ~ spl55_1878
| ~ spl55_1918 ),
inference(forward_subsumption_resolution,[],[f48395,f48027]) ).
fof(f48782,plain,
( ~ ron(sK6,vd1295)
| ~ ron(sK5,vd1295)
| ~ spl55_1919 ),
inference(resolution,[],[f48406,f687]) ).
fof(f48786,plain,
( ~ ron(sK5,vd1295)
| ~ spl55_1919 ),
inference(forward_subsumption_resolution,[],[f48782,f938]) ).
fof(f48788,plain,
( $false
| ~ spl55_1919 ),
inference(forward_subsumption_resolution,[],[f48786,f927]) ).
fof(f48789,plain,
~ spl55_1919,
inference(avatar_contradiction_clause,[],[f48788]) ).
fof(f48794,plain,
( spl55_1919
| ~ spl55_1878
| ~ spl55_1918 ),
inference(avatar_split_clause,[],[f48496,f48394,f48026,f48405]) ).
fof(f48902,plain,
( vd684 != vangle(sK6,sK4,vd1329)
| spl55_442 ),
inference(avatar_component_clause,[],[f13373]) ).
fof(f49583,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X1,vd1295)
| X0 = X3
| X0 = X2
| X0 = X4
| X0 = X1
| ~ ron(X3,vd1297)
| ~ ron(X4,vd1297)
| ~ ron(X2,vd1295)
| rR(X0,X1,X2)
| ~ ron(X0,vd1295)
| vangle(X1,X0,X4) = vangle(X2,X0,X3)
| rR(X0,X4,X3)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f1912,f687]) ).
fof(f49588,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| X0 = X2
| X0 = X3
| sK5 = X0
| ~ ron(X1,vd1297)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1295)
| rR(X0,sK5,X2)
| ~ ron(X0,vd1295)
| vangle(X2,X0,X1) = vangle(sK5,X0,X3)
| rR(X0,X3,X1)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(sK5)
| ~ rpoint(X0) ),
inference(resolution,[],[f49583,f927]) ).
fof(f49591,plain,
! [X2,X3,X0,X1] :
( ~ ron(X1,vd1297)
| X0 = X2
| X0 = X3
| sK5 = X0
| X0 = X1
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1295)
| rR(X0,sK5,X2)
| ~ ron(X0,vd1295)
| vangle(X2,X0,X1) = vangle(sK5,X0,X3)
| rR(X0,X3,X1)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f49588,f567]) ).
fof(f49689,plain,
( ron(sK5,vd1297)
| ~ ron(vd1300,vd1297)
| ~ ron(sK6,vd1297)
| ~ spl55_1894 ),
inference(resolution,[],[f48206,f685]) ).
fof(f49756,definition,
( spl55_1959
<=> vangle(sK4,sK5,vd1303) = vangle(vd1303,sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl55_1959])],[avatar_definition]) ).
fof(f49757,plain,
( vangle(sK4,sK5,vd1303) = vangle(vd1303,sK5,sK4)
| ~ spl55_1959 ),
inference(avatar_component_clause,[],[f49756]) ).
fof(f49758,plain,
( spl55_1959
| spl55_61 ),
inference(avatar_split_clause,[],[f5270,f2214,f49756]) ).
fof(f49970,plain,
( ron(sK4,vd1295)
| ~ spl55_129 ),
inference(forward_subsumption_resolution,[],[f22552,f569]) ).
fof(f50505,definition,
( spl55_2062
<=> ron(sK4,vd1295) ),
introduced(definition,[new_symbols(definition,[spl55_2062])],[avatar_definition]) ).
fof(f50506,plain,
( ron(sK4,vd1295)
| ~ spl55_2062 ),
inference(avatar_component_clause,[],[f50505]) ).
fof(f50508,plain,
( ron(vd1303,vd1295)
| ~ spl55_45 ),
inference(avatar_component_clause,[],[f2073]) ).
fof(f50520,definition,
( spl55_2064
<=> ! [X0] :
( ron(sK4,X0)
| ~ rline(X0)
| ~ ron(vd1303,X0)
| ~ ron(sK6,X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_2064])],[avatar_definition]) ).
fof(f50521,plain,
( ! [X0] :
( ~ rline(X0)
| ron(sK4,X0)
| ~ ron(vd1303,X0)
| ~ ron(sK6,X0) )
| ~ spl55_2064 ),
inference(avatar_component_clause,[],[f50520]) ).
fof(f50522,plain,
( spl55_61
| spl55_2064
| ~ spl55_65 ),
inference(avatar_split_clause,[],[f48007,f2264,f50520,f2214]) ).
fof(f50526,plain,
( ~ rR(vd1303,sK4,sK6)
| spl55_68 ),
inference(avatar_component_clause,[],[f2329]) ).
fof(f50612,plain,
( ron(sK5,vd1297)
| ~ ron(vd1300,vd1297)
| ~ spl55_1894 ),
inference(forward_subsumption_resolution,[],[f49689,f935]) ).
fof(f50691,plain,
( spl55_2062
| ~ spl55_129 ),
inference(avatar_split_clause,[],[f49970,f4652,f50505]) ).
fof(f51208,definition,
( spl55_2112
<=> vd684 = vangle(sK6,vd1300,sK4) ),
introduced(definition,[new_symbols(definition,[spl55_2112])],[avatar_definition]) ).
fof(f51209,plain,
( vd684 = vangle(sK6,vd1300,sK4)
| ~ spl55_2112 ),
inference(avatar_component_clause,[],[f51208]) ).
fof(f52713,plain,
( ! [X0] :
( vd684 != vd684
| ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| vd1303 = sK6
| sK4 = sK6
| ~ rline(X0)
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| spl55_21 ),
inference(superposition,[],[f1049,f3986]) ).
fof(f52716,plain,
( ! [X0] :
( ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| vd1303 = sK6
| sK4 = sK6
| ~ rline(X0)
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| spl55_21 ),
inference(trivial_inequality_removal,[],[f52713]) ).
fof(f52717,plain,
( ! [X0] :
( ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| sK4 = sK6
| ~ rline(X0)
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f52716,f894]) ).
fof(f52718,plain,
( ! [X0] :
( ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(vd1303)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f52717,f1822]) ).
fof(f52719,plain,
( ! [X0] :
( ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6) )
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f52718,f561]) ).
fof(f52720,plain,
( ! [X0] :
( ron(vd1303,X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK6) )
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f52719,f569]) ).
fof(f52721,plain,
( ! [X0] :
( ~ rline(X0)
| ~ ron(sK4,X0)
| ~ ron(sK6,X0)
| ron(vd1303,X0) )
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f52720,f565]) ).
fof(f52742,plain,
( rR(vd1303,sK4,sK6)
| ~ rpoint(sK4)
| ~ rpoint(vd1303)
| ~ rpoint(sK6)
| ~ spl55_66 ),
inference(resolution,[],[f2268,f1115]) ).
fof(f52798,plain,
( ~ rpoint(sK6)
| ~ rpoint(sK4)
| ~ rR(sK4,vd1303,sK6)
| ~ spl55_68 ),
inference(resolution,[],[f2330,f1959]) ).
fof(f52848,plain,
( ~ rpoint(sK4)
| ~ rR(sK4,vd1303,sK6)
| ~ spl55_68 ),
inference(forward_subsumption_resolution,[],[f52798,f565]) ).
fof(f52867,plain,
( ~ rR(sK4,vd1303,sK6)
| ~ spl55_68 ),
inference(forward_subsumption_resolution,[],[f52848,f569]) ).
fof(f52904,plain,
( $false
| ~ spl55_68 ),
inference(forward_subsumption_resolution,[],[f52867,f1901]) ).
fof(f52905,plain,
~ spl55_68,
inference(avatar_contradiction_clause,[],[f52904]) ).
fof(f52925,plain,
( ~ rpoint(sK4)
| ~ rpoint(vd1303)
| ~ rpoint(sK6)
| ~ spl55_66
| spl55_68 ),
inference(forward_subsumption_resolution,[],[f52742,f50526]) ).
fof(f52926,plain,
( ~ rpoint(vd1303)
| ~ rpoint(sK6)
| ~ spl55_66
| spl55_68 ),
inference(forward_subsumption_resolution,[],[f52925,f569]) ).
fof(f52927,plain,
( ~ rpoint(sK6)
| ~ spl55_66
| spl55_68 ),
inference(forward_subsumption_resolution,[],[f52926,f561]) ).
fof(f52928,plain,
( $false
| ~ spl55_66
| spl55_68 ),
inference(forward_subsumption_resolution,[],[f52927,f565]) ).
fof(f52929,plain,
( ~ spl55_66
| spl55_68 ),
inference(avatar_contradiction_clause,[],[f52928]) ).
fof(f52956,plain,
( ron(sK4,vd1295)
| ~ ron(vd1303,vd1295)
| ~ ron(sK6,vd1295)
| ~ spl55_2064 ),
inference(resolution,[],[f50521,f687]) ).
fof(f53359,plain,
( ~ ron(sK4,vd1295)
| ~ ron(sK6,vd1295)
| ron(vd1303,vd1295)
| spl55_21 ),
inference(resolution,[],[f52721,f687]) ).
fof(f53401,plain,
! [X2,X0,X1] :
( X0 = X1
| X0 = X2
| sK5 = X0
| sK4 = X0
| ~ ron(X2,vd1297)
| ~ ron(X1,vd1295)
| rR(X0,sK5,X1)
| ~ ron(X0,vd1295)
| vangle(sK5,X0,X2) = vangle(X1,X0,sK4)
| rR(X0,X2,sK4)
| ~ rpoint(sK4)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f49591,f934]) ).
fof(f53405,plain,
! [X2,X0,X1] :
( ~ ron(X2,vd1297)
| X0 = X2
| sK5 = X0
| sK4 = X0
| X0 = X1
| ~ ron(X1,vd1295)
| rR(X0,sK5,X1)
| ~ ron(X0,vd1295)
| vangle(sK5,X0,X2) = vangle(X1,X0,sK4)
| rR(X0,X2,sK4)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f53401,f569]) ).
fof(f54815,plain,
( ron(sK4,vd1295)
| ~ ron(vd1300,vd1295)
| ~ ron(sK6,vd1295)
| ~ spl55_1903 ),
inference(resolution,[],[f48275,f687]) ).
fof(f55473,plain,
! [X0] :
( vd684 != vangle(sK6,sK4,vd1329)
| ~ rR(sK5,vd1303,sK6)
| ~ ron(vd1303,X0)
| ~ ron(sK5,X0)
| sK5 = sK6
| vd1303 = sK5
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(vd1303)
| ~ rpoint(sK5) ),
inference(superposition,[],[f1045,f3309]) ).
fof(f56179,definition,
( spl55_2311
<=> ! [X0] :
( ~ ron(sK5,X0)
| ~ rline(X0)
| ~ ron(vd1303,X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_2311])],[avatar_definition]) ).
fof(f56180,plain,
( ! [X0] :
( ~ rline(X0)
| ~ ron(sK5,X0)
| ~ ron(vd1303,X0) )
| ~ spl55_2311 ),
inference(avatar_component_clause,[],[f56179]) ).
fof(f57859,plain,
( ! [X0] :
( ~ rR(sK5,vd1303,sK6)
| ~ ron(vd1303,X0)
| ~ ron(sK5,X0)
| sK5 = sK6
| vd1303 = sK5
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(vd1303)
| ~ rpoint(sK5) )
| ~ spl55_442 ),
inference(forward_subsumption_resolution,[],[f55473,f13374]) ).
fof(f57863,definition,
( spl55_2423
<=> vd684 = vangle(vd1303,sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl55_2423])],[avatar_definition]) ).
fof(f57864,plain,
( vd684 = vangle(vd1303,sK5,sK4)
| ~ spl55_2423 ),
inference(avatar_component_clause,[],[f57863]) ).
fof(f57873,definition,
( spl55_2424
<=> rR(sK5,sK6,vd1303) ),
introduced(definition,[new_symbols(definition,[spl55_2424])],[avatar_definition]) ).
fof(f57880,plain,
( ! [X0] :
( ~ rR(sK5,vd1303,sK6)
| ~ ron(vd1303,X0)
| ~ ron(sK5,X0)
| vd1303 = sK5
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(vd1303)
| ~ rpoint(sK5) )
| ~ spl55_442 ),
inference(forward_subsumption_resolution,[],[f57859,f928]) ).
fof(f57885,plain,
( ! [X0] :
( ~ rR(sK5,vd1303,sK6)
| ~ ron(vd1303,X0)
| ~ ron(sK5,X0)
| vd1303 = sK5
| ~ rline(X0)
| ~ rpoint(vd1303)
| ~ rpoint(sK5) )
| ~ spl55_442 ),
inference(forward_subsumption_resolution,[],[f57880,f565]) ).
fof(f57889,plain,
( ! [X0] :
( ~ rR(sK5,vd1303,sK6)
| ~ ron(vd1303,X0)
| ~ ron(sK5,X0)
| vd1303 = sK5
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl55_442 ),
inference(forward_subsumption_resolution,[],[f57885,f561]) ).
fof(f57893,plain,
( ! [X0] :
( ~ rR(sK5,vd1303,sK6)
| ~ ron(vd1303,X0)
| ~ ron(sK5,X0)
| vd1303 = sK5
| ~ rline(X0) )
| ~ spl55_442 ),
inference(forward_subsumption_resolution,[],[f57889,f567]) ).
fof(f57898,plain,
( spl55_44
| spl55_2311
| ~ spl55_46
| ~ spl55_442 ),
inference(avatar_split_clause,[],[f57893,f13373,f2092,f56179,f2070]) ).
fof(f58443,plain,
( vangle(sK6,sK4,vd1329) != vplus(vangle(sK4,sK5,vd1303),vd684)
| ~ spl55_130 ),
inference(superposition,[],[f1884,f4656]) ).
fof(f58444,plain,
( ! [X0] :
( vd684 != vd684
| ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| sK4 = sK5
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ rpoint(sK5) )
| ~ spl55_130 ),
inference(superposition,[],[f1049,f4656]) ).
fof(f58447,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| sK4 = sK5
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ rpoint(sK5) )
| ~ spl55_130 ),
inference(trivial_inequality_removal,[],[f58444]) ).
fof(f58449,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ rpoint(sK5) )
| ~ spl55_130 ),
inference(forward_subsumption_resolution,[],[f58447,f882]) ).
fof(f58450,plain,
( vangle(sK6,sK4,vd1329) != vplus(vangle(vd1303,sK5,sK4),vd684)
| ~ spl55_130
| ~ spl55_1959 ),
inference(forward_demodulation,[],[f58443,f49757]) ).
fof(f58452,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ rpoint(sK5) )
| ~ spl55_130 ),
inference(forward_subsumption_resolution,[],[f58449,f928]) ).
fof(f58453,plain,
( vangle(sK6,sK4,vd1329) != vplus(vd684,vd684)
| ~ spl55_130
| ~ spl55_1959
| ~ spl55_2423 ),
inference(forward_demodulation,[],[f58450,f57864]) ).
fof(f58455,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5) )
| ~ spl55_130 ),
inference(forward_subsumption_resolution,[],[f58452,f569]) ).
fof(f58456,plain,
( vd684 != vangle(sK6,sK4,vd1329)
| ~ spl55_130
| ~ spl55_1959
| ~ spl55_2423 ),
inference(forward_demodulation,[],[f58453,f3588]) ).
fof(f58458,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK5) )
| ~ spl55_130 ),
inference(forward_subsumption_resolution,[],[f58455,f565]) ).
fof(f58460,plain,
( ! [X0] :
( ~ rline(X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| ron(sK4,X0) )
| ~ spl55_130 ),
inference(forward_subsumption_resolution,[],[f58458,f567]) ).
fof(f58461,plain,
( ~ rR(sK5,sK6,sK4)
| spl55_129 ),
inference(avatar_component_clause,[],[f4652]) ).
fof(f58464,plain,
( ~ ron(sK6,vd1295)
| ~ ron(sK5,vd1295)
| ron(sK4,vd1295)
| ~ spl55_130 ),
inference(resolution,[],[f58460,f687]) ).
fof(f58648,definition,
( spl55_2430
<=> rR(sK5,vd1303,sK4) ),
introduced(definition,[new_symbols(definition,[spl55_2430])],[avatar_definition]) ).
fof(f59894,plain,
( ! [X0] :
( vd684 != vd684
| ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1300,X0)
| vd1300 = sK4
| vd1300 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ rpoint(vd1300) )
| ~ spl55_2112 ),
inference(superposition,[],[f1049,f51209]) ).
fof(f59897,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1300,X0)
| vd1300 = sK4
| vd1300 = sK6
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ rpoint(vd1300) )
| ~ spl55_2112 ),
inference(trivial_inequality_removal,[],[f59894]) ).
fof(f60851,plain,
( $false
| spl55_21
| spl55_153
| ~ spl55_2062 ),
inference(unit_resulting_resolution,[],[f4339,f565,f569,f567,f687,f565,f569,f1822,f938,f927,f882,f48425,f30002,f30005,f39665,f50506]) ).
fof(f60852,plain,
( $false
| spl55_21
| spl55_574
| ~ spl55_2062 ),
inference(unit_resulting_resolution,[],[f4339,f565,f567,f569,f565,f569,f687,f1822,f938,f927,f882,f48472,f30002,f30005,f39665,f50506]) ).
fof(f60961,plain,
( spl55_21
| spl55_153
| ~ spl55_2062 ),
inference(avatar_contradiction_clause,[],[f60851]) ).
fof(f60962,plain,
( spl55_21
| spl55_574
| ~ spl55_2062 ),
inference(avatar_contradiction_clause,[],[f60852]) ).
fof(f61069,plain,
( ron(sK4,vd1295)
| ~ ron(sK6,vd1295)
| ~ spl55_45
| ~ spl55_2064 ),
inference(forward_subsumption_resolution,[],[f52956,f50508]) ).
fof(f61071,plain,
( ron(sK4,vd1295)
| ~ ron(sK6,vd1295)
| ~ spl55_1903 ),
inference(forward_subsumption_resolution,[],[f54815,f933]) ).
fof(f61078,plain,
( ~ ron(sK5,vd1295)
| ron(sK4,vd1295)
| ~ spl55_130 ),
inference(forward_subsumption_resolution,[],[f58464,f938]) ).
fof(f61085,plain,
( ron(sK4,vd1295)
| ~ spl55_45
| ~ spl55_2064 ),
inference(forward_subsumption_resolution,[],[f61069,f938]) ).
fof(f61086,plain,
( ron(sK4,vd1295)
| ~ spl55_1903 ),
inference(forward_subsumption_resolution,[],[f61071,f938]) ).
fof(f61093,plain,
( ron(sK4,vd1295)
| ~ spl55_130 ),
inference(forward_subsumption_resolution,[],[f61078,f927]) ).
fof(f61100,plain,
( spl55_2062
| ~ spl55_45
| ~ spl55_2064 ),
inference(avatar_split_clause,[],[f61085,f50520,f2073,f50505]) ).
fof(f61101,plain,
( spl55_2062
| ~ spl55_1903 ),
inference(avatar_split_clause,[],[f61086,f48274,f50505]) ).
fof(f61107,plain,
( spl55_2062
| ~ spl55_130 ),
inference(avatar_split_clause,[],[f61093,f4655,f50505]) ).
fof(f61119,definition,
( spl55_2548
<=> ron(sK5,vd1297) ),
introduced(definition,[new_symbols(definition,[spl55_2548])],[avatar_definition]) ).
fof(f61120,plain,
( ron(sK5,vd1297)
| ~ spl55_2548 ),
inference(avatar_component_clause,[],[f61119]) ).
fof(f61123,definition,
( spl55_2549
<=> ron(vd1300,vd1297) ),
introduced(definition,[new_symbols(definition,[spl55_2549])],[avatar_definition]) ).
fof(f61125,plain,
( ~ spl55_2549
| spl55_2548
| ~ spl55_1894 ),
inference(avatar_split_clause,[],[f50612,f48205,f61119,f61123]) ).
fof(f61126,plain,
( ~ ron(sK5,vd1297)
| spl55_2548 ),
inference(avatar_component_clause,[],[f61119]) ).
fof(f61152,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1300,X0)
| vd1300 = sK4
| ~ rline(X0)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ rpoint(vd1300) )
| spl55_20
| ~ spl55_2112 ),
inference(forward_subsumption_resolution,[],[f59897,f1817]) ).
fof(f61165,plain,
( ~ ron(sK4,vd1295)
| ron(vd1303,vd1295)
| spl55_21 ),
inference(forward_subsumption_resolution,[],[f53359,f938]) ).
fof(f61172,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1300,X0)
| vd1300 = sK4
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(vd1300) )
| spl55_20
| ~ spl55_2112 ),
inference(forward_subsumption_resolution,[],[f61152,f569]) ).
fof(f61184,plain,
( ~ ron(sK4,vd1295)
| spl55_21
| spl55_45 ),
inference(forward_subsumption_resolution,[],[f61165,f2074]) ).
fof(f61190,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1300,X0)
| vd1300 = sK4
| ~ rline(X0)
| ~ rpoint(vd1300) )
| spl55_20
| ~ spl55_2112 ),
inference(forward_subsumption_resolution,[],[f61172,f565]) ).
fof(f61202,plain,
( ! [X0] :
( ron(sK4,X0)
| ~ ron(sK6,X0)
| ~ ron(vd1300,X0)
| vd1300 = sK4
| ~ rline(X0) )
| spl55_20
| ~ spl55_2112 ),
inference(forward_subsumption_resolution,[],[f61190,f564]) ).
fof(f61206,plain,
( spl55_84
| spl55_1903
| spl55_20
| ~ spl55_2112 ),
inference(avatar_split_clause,[],[f61202,f51208,f1816,f48274,f2965]) ).
fof(f61266,plain,
( rR(sK5,sK6,sK4)
| sK4 = sK5
| sK5 = sK6
| vd684 = vangle(sK6,sK5,sK4)
| ~ rpoint(sK5)
| ~ spl55_2548 ),
inference(resolution,[],[f61120,f1982]) ).
fof(f61330,plain,
( sK4 = sK5
| sK5 = sK6
| vd684 = vangle(sK6,sK5,sK4)
| ~ rpoint(sK5)
| spl55_129
| ~ spl55_2548 ),
inference(forward_subsumption_resolution,[],[f61266,f58461]) ).
fof(f61342,plain,
( sK5 = sK6
| vd684 = vangle(sK6,sK5,sK4)
| ~ rpoint(sK5)
| spl55_129
| ~ spl55_2548 ),
inference(forward_subsumption_resolution,[],[f61330,f882]) ).
fof(f61348,plain,
( vd684 = vangle(sK6,sK5,sK4)
| ~ rpoint(sK5)
| spl55_129
| ~ spl55_2548 ),
inference(forward_subsumption_resolution,[],[f61342,f928]) ).
fof(f61354,plain,
( ~ rpoint(sK5)
| spl55_129
| spl55_130
| ~ spl55_2548 ),
inference(forward_subsumption_resolution,[],[f61348,f48377]) ).
fof(f61360,plain,
( $false
| spl55_129
| spl55_130
| ~ spl55_2548 ),
inference(forward_subsumption_resolution,[],[f61354,f567]) ).
fof(f61361,plain,
( spl55_129
| spl55_130
| ~ spl55_2548 ),
inference(avatar_contradiction_clause,[],[f61360]) ).
fof(f61548,plain,
! [X0,X1] :
( sK6 = X0
| sK5 = X0
| sK4 = X0
| X0 = X1
| ~ ron(X1,vd1295)
| rR(X0,sK5,X1)
| ~ ron(X0,vd1295)
| vangle(X1,X0,sK4) = vangle(sK5,X0,sK6)
| rR(X0,sK6,sK4)
| ~ rpoint(X1)
| ~ rpoint(sK6)
| ~ rpoint(X0) ),
inference(resolution,[],[f53405,f935]) ).
fof(f61550,plain,
! [X0,X1] :
( ~ ron(X1,vd1295)
| sK5 = X0
| sK4 = X0
| X0 = X1
| sK6 = X0
| rR(X0,sK5,X1)
| ~ ron(X0,vd1295)
| vangle(X1,X0,sK4) = vangle(sK5,X0,sK6)
| rR(X0,sK6,sK4)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f61548,f565]) ).
fof(f61613,plain,
! [X0] :
( sK5 = X0
| sK4 = X0
| sK6 = X0
| sK6 = X0
| rR(X0,sK5,sK6)
| ~ ron(X0,vd1295)
| vangle(sK5,X0,sK6) = vangle(sK6,X0,sK4)
| rR(X0,sK6,sK4)
| ~ rpoint(sK6)
| ~ rpoint(X0) ),
inference(resolution,[],[f61550,f938]) ).
fof(f61614,plain,
! [X0] :
( sK5 = X0
| sK4 = X0
| sK6 = X0
| rR(X0,sK5,sK6)
| ~ ron(X0,vd1295)
| vangle(sK5,X0,sK6) = vangle(sK6,X0,sK4)
| rR(X0,sK6,sK4)
| ~ rpoint(sK6)
| ~ rpoint(X0) ),
inference(duplicate_literal_removal,[],[f61613]) ).
fof(f61616,plain,
! [X0] :
( ~ ron(X0,vd1295)
| sK4 = X0
| sK6 = X0
| rR(X0,sK5,sK6)
| sK5 = X0
| vangle(sK5,X0,sK6) = vangle(sK6,X0,sK4)
| rR(X0,sK6,sK4)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f61614,f565]) ).
fof(f61808,plain,
( vd1300 = sK4
| vd1300 = sK6
| rR(vd1300,sK5,sK6)
| vd1300 = sK5
| vangle(sK6,vd1300,sK4) = vangle(sK5,vd1300,sK6)
| rR(vd1300,sK6,sK4)
| ~ rpoint(vd1300) ),
inference(resolution,[],[f61616,f933]) ).
fof(f61811,plain,
( vd1300 = sK4
| rR(vd1300,sK5,sK6)
| vd1300 = sK5
| vangle(sK6,vd1300,sK4) = vangle(sK5,vd1300,sK6)
| rR(vd1300,sK6,sK4)
| ~ rpoint(vd1300)
| spl55_20 ),
inference(forward_subsumption_resolution,[],[f61808,f1817]) ).
fof(f61812,plain,
( vd1300 = sK4
| vd1300 = sK5
| vangle(sK6,vd1300,sK4) = vangle(sK5,vd1300,sK6)
| rR(vd1300,sK6,sK4)
| ~ rpoint(vd1300)
| spl55_20
| spl55_1896 ),
inference(forward_subsumption_resolution,[],[f61811,f48221]) ).
fof(f61817,plain,
( vd1300 = sK4
| vd1300 = sK5
| vangle(sK6,vd1300,sK4) = vangle(sK5,vd1300,sK6)
| rR(vd1300,sK6,sK4)
| spl55_20
| spl55_1896 ),
inference(forward_subsumption_resolution,[],[f61812,f564]) ).
fof(f61818,plain,
( vd684 = vangle(sK6,vd1300,sK4)
| vd1300 = sK4
| vd1300 = sK5
| rR(vd1300,sK6,sK4)
| spl55_20
| ~ spl55_94
| spl55_1896 ),
inference(forward_demodulation,[],[f61817,f3312]) ).
fof(f61819,plain,
( rR(vd1300,sK6,sK4)
| ~ spl55_1902 ),
inference(avatar_component_clause,[],[f48270]) ).
fof(f61820,plain,
( spl55_1902
| spl55_53
| spl55_84
| spl55_2112
| spl55_20
| ~ spl55_94
| spl55_1896 ),
inference(avatar_split_clause,[],[f61818,f48220,f3311,f1816,f51208,f2965,f2154,f48270]) ).
fof(f61854,plain,
( ~ ron(sK6,vd1295)
| ron(sK4,vd1295)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ spl55_1902 ),
inference(resolution,[],[f61819,f8499]) ).
fof(f61912,plain,
( ron(sK4,vd1295)
| ~ rpoint(sK4)
| ~ rpoint(sK6)
| ~ spl55_1902 ),
inference(forward_subsumption_resolution,[],[f61854,f938]) ).
fof(f61945,plain,
( ~ rpoint(sK4)
| ~ rpoint(sK6)
| spl55_21
| spl55_45
| ~ spl55_1902 ),
inference(forward_subsumption_resolution,[],[f61912,f61184]) ).
fof(f61972,plain,
( ~ rpoint(sK6)
| spl55_21
| spl55_45
| ~ spl55_1902 ),
inference(forward_subsumption_resolution,[],[f61945,f569]) ).
fof(f61992,plain,
( $false
| spl55_21
| spl55_45
| ~ spl55_1902 ),
inference(forward_subsumption_resolution,[],[f61972,f565]) ).
fof(f61993,plain,
( spl55_21
| spl55_45
| ~ spl55_1902 ),
inference(avatar_contradiction_clause,[],[f61992]) ).
fof(f63281,plain,
( ~ ron(sK4,vd1297)
| ron(sK5,vd1297)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ spl55_153 ),
inference(resolution,[],[f5061,f8488]) ).
fof(f63389,plain,
( rR(sK5,vd1303,sK4)
| sK4 = sK5
| vd1303 = sK5
| vd684 = vangle(vd1303,sK5,sK4)
| ~ rpoint(sK5)
| ~ spl55_2548 ),
inference(resolution,[],[f61120,f1983]) ).
fof(f63511,plain,
( $false
| ~ spl55_130
| ~ spl55_442
| ~ spl55_1959
| ~ spl55_2423 ),
inference(forward_subsumption_resolution,[],[f58456,f13374]) ).
fof(f63512,plain,
( ~ spl55_130
| ~ spl55_442
| ~ spl55_1959
| ~ spl55_2423 ),
inference(avatar_contradiction_clause,[],[f63511]) ).
fof(f63513,plain,
( rR(sK5,vd1303,sK4)
| vd1303 = sK5
| vd684 = vangle(vd1303,sK5,sK4)
| ~ rpoint(sK5)
| ~ spl55_2548 ),
inference(forward_subsumption_resolution,[],[f63389,f882]) ).
fof(f63514,plain,
( rR(sK5,vd1303,sK4)
| vd1303 = sK5
| vd684 = vangle(vd1303,sK5,sK4)
| ~ spl55_2548 ),
inference(forward_subsumption_resolution,[],[f63513,f567]) ).
fof(f63515,plain,
( rR(sK5,vd1303,sK4)
| ~ spl55_2430 ),
inference(avatar_component_clause,[],[f58648]) ).
fof(f63516,plain,
( spl55_2423
| spl55_44
| spl55_2430
| ~ spl55_2548 ),
inference(avatar_split_clause,[],[f63514,f61119,f58648,f2070,f57863]) ).
fof(f63519,plain,
( $false
| spl55_46
| ~ spl55_2430 ),
inference(unit_resulting_resolution,[],[f1398,f561,f569,f565,f567,f2093,f1901,f63515]) ).
fof(f63536,plain,
( spl55_46
| ~ spl55_2430 ),
inference(avatar_contradiction_clause,[],[f63519]) ).
fof(f63605,plain,
( ~ ron(sK5,vd1295)
| ~ ron(vd1303,vd1295)
| ~ spl55_2311 ),
inference(resolution,[],[f56180,f687]) ).
fof(f63608,plain,
( ~ ron(vd1303,vd1295)
| ~ spl55_2311 ),
inference(forward_subsumption_resolution,[],[f63605,f927]) ).
fof(f63610,plain,
( $false
| ~ spl55_45
| ~ spl55_2311 ),
inference(forward_subsumption_resolution,[],[f63608,f50508]) ).
fof(f63611,plain,
( ~ spl55_45
| ~ spl55_2311 ),
inference(avatar_contradiction_clause,[],[f63610]) ).
fof(f63683,plain,
( rR(sK6,sK4,vd1303)
| ~ spl55_44
| ~ spl55_153 ),
inference(superposition,[],[f5061,f2071]) ).
fof(f63977,plain,
( $false
| ~ spl55_44
| ~ spl55_153 ),
inference(forward_subsumption_resolution,[],[f63683,f877]) ).
fof(f63978,plain,
( ~ spl55_44
| ~ spl55_153 ),
inference(avatar_contradiction_clause,[],[f63977]) ).
fof(f64080,plain,
( ron(sK5,vd1297)
| ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ spl55_153 ),
inference(forward_subsumption_resolution,[],[f63281,f934]) ).
fof(f64092,plain,
( ron(vd1303,vd1295)
| spl55_21
| ~ spl55_2062 ),
inference(forward_subsumption_resolution,[],[f61165,f50506]) ).
fof(f64100,plain,
( ~ rpoint(sK5)
| ~ rpoint(sK4)
| ~ spl55_153
| spl55_2548 ),
inference(forward_subsumption_resolution,[],[f64080,f61126]) ).
fof(f64116,plain,
( $false
| spl55_21
| spl55_45
| ~ spl55_2062 ),
inference(forward_subsumption_resolution,[],[f64092,f2074]) ).
fof(f64117,plain,
( spl55_21
| spl55_45
| ~ spl55_2062 ),
inference(avatar_contradiction_clause,[],[f64116]) ).
fof(f64125,plain,
( ~ rpoint(sK4)
| ~ spl55_153
| spl55_2548 ),
inference(forward_subsumption_resolution,[],[f64100,f567]) ).
fof(f64137,plain,
( $false
| ~ spl55_153
| spl55_2548 ),
inference(forward_subsumption_resolution,[],[f64125,f569]) ).
fof(f64138,plain,
( ~ spl55_153
| spl55_2548 ),
inference(avatar_contradiction_clause,[],[f64137]) ).
fof(f64345,plain,
( rR(sK5,sK6,vd1303)
| vd1303 = sK5
| sK5 = sK6
| vd684 = vangle(sK6,sK5,vd1303)
| ~ rpoint(sK5)
| ~ spl55_2548 ),
inference(resolution,[],[f61120,f2242]) ).
fof(f64447,plain,
( rR(sK5,sK6,vd1303)
| vd1303 = sK5
| vd684 = vangle(sK6,sK5,vd1303)
| ~ rpoint(sK5)
| ~ spl55_2548 ),
inference(forward_subsumption_resolution,[],[f64345,f928]) ).
fof(f64455,plain,
( rR(sK5,sK6,vd1303)
| vd1303 = sK5
| vd684 = vangle(sK6,sK5,vd1303)
| ~ spl55_2548 ),
inference(forward_subsumption_resolution,[],[f64447,f567]) ).
fof(f64457,plain,
( vd684 = vangle(sK6,sK4,vd1329)
| rR(sK5,sK6,vd1303)
| vd1303 = sK5
| ~ spl55_2548 ),
inference(forward_demodulation,[],[f64455,f868]) ).
fof(f64459,plain,
( rR(sK5,sK6,vd1303)
| vd1303 = sK5
| spl55_442
| ~ spl55_2548 ),
inference(forward_subsumption_resolution,[],[f64457,f48902]) ).
fof(f64461,plain,
( rR(sK5,sK6,vd1303)
| ~ spl55_2424 ),
inference(avatar_component_clause,[],[f57873]) ).
fof(f64462,plain,
( spl55_44
| spl55_2424
| spl55_442
| ~ spl55_2548 ),
inference(avatar_split_clause,[],[f64459,f61119,f13373,f57873,f2070]) ).
fof(f64466,plain,
( $false
| ~ spl55_153
| ~ spl55_2424 ),
inference(unit_resulting_resolution,[],[f2201,f561,f565,f567,f877,f5061,f64461]) ).
fof(f64498,plain,
( ~ spl55_153
| ~ spl55_2424 ),
inference(avatar_contradiction_clause,[],[f64466]) ).
fof(f64655,plain,
( spl55_2549
| ~ spl55_84 ),
inference(avatar_split_clause,[],[f3111,f2965,f61123]) ).
cnf(s40,plain,
~ spl55_21,
inference(sat_conversion,[],[f1883]) ).
cnf(s46,plain,
( ~ spl55_20
| spl55_39 ),
inference(sat_conversion,[],[f2031]) ).
cnf(s58,plain,
( spl55_61
| spl55_65
| spl55_66 ),
inference(sat_conversion,[],[f2269]) ).
cnf(s64,plain,
~ spl55_61,
inference(sat_conversion,[],[f2314]) ).
cnf(s77,plain,
~ spl55_39,
inference(sat_conversion,[],[f2426]) ).
cnf(s126,plain,
( spl55_20
| spl55_39
| spl55_53
| spl55_94 ),
inference(sat_conversion,[],[f3313]) ).
cnf(s173,plain,
~ spl55_53,
inference(sat_conversion,[],[f4540]) ).
cnf(s178,plain,
( spl55_20
| spl55_22
| spl55_126 ),
inference(sat_conversion,[],[f4598]) ).
cnf(s214,plain,
( spl55_53
| ~ spl55_126
| spl55_152 ),
inference(sat_conversion,[],[f5026]) ).
cnf(s801,plain,
( ~ spl55_129
| ~ spl55_574 ),
inference(sat_conversion,[],[f19128]) ).
cnf(s862,plain,
~ spl55_22,
inference(sat_conversion,[],[f19986]) ).
cnf(s2596,plain,
( spl55_20
| spl55_53
| ~ spl55_94
| spl55_1878
| ~ spl55_1896 ),
inference(sat_conversion,[],[f48222]) ).
cnf(s2643,plain,
( spl55_20
| ~ spl55_126
| spl55_1918 ),
inference(sat_conversion,[],[f48423]) ).
cnf(s2644,plain,
( spl55_20
| ~ spl55_152
| spl55_1894 ),
inference(sat_conversion,[],[f48424]) ).
cnf(s2753,plain,
~ spl55_1919,
inference(sat_conversion,[],[f48789]) ).
cnf(s2756,plain,
( ~ spl55_1878
| ~ spl55_1918
| spl55_1919 ),
inference(sat_conversion,[],[f48794]) ).
cnf(s2901,plain,
( spl55_61
| spl55_1959 ),
inference(sat_conversion,[],[f49758]) ).
cnf(s3042,plain,
( spl55_61
| ~ spl55_65
| spl55_2064 ),
inference(sat_conversion,[],[f50522]) ).
cnf(s3077,plain,
( ~ spl55_129
| spl55_2062 ),
inference(sat_conversion,[],[f50691]) ).
cnf(s3393,plain,
~ spl55_68,
inference(sat_conversion,[],[f52905]) ).
cnf(s3400,plain,
( ~ spl55_66
| spl55_68 ),
inference(sat_conversion,[],[f52929]) ).
cnf(s3792,plain,
( spl55_44
| ~ spl55_46
| ~ spl55_442
| spl55_2311 ),
inference(sat_conversion,[],[f57898]) ).
cnf(s4001,plain,
( spl55_21
| spl55_153
| ~ spl55_2062 ),
inference(sat_conversion,[],[f60961]) ).
cnf(s4002,plain,
( spl55_21
| spl55_574
| ~ spl55_2062 ),
inference(sat_conversion,[],[f60962]) ).
cnf(s4016,plain,
( ~ spl55_45
| spl55_2062
| ~ spl55_2064 ),
inference(sat_conversion,[],[f61100]) ).
cnf(s4017,plain,
( ~ spl55_1903
| spl55_2062 ),
inference(sat_conversion,[],[f61101]) ).
cnf(s4021,plain,
( ~ spl55_130
| spl55_2062 ),
inference(sat_conversion,[],[f61107]) ).
cnf(s4027,plain,
( ~ spl55_1894
| spl55_2548
| ~ spl55_2549 ),
inference(sat_conversion,[],[f61125]) ).
cnf(s4057,plain,
( spl55_20
| spl55_84
| spl55_1903
| ~ spl55_2112 ),
inference(sat_conversion,[],[f61206]) ).
cnf(s4092,plain,
( spl55_129
| spl55_130
| ~ spl55_2548 ),
inference(sat_conversion,[],[f61361]) ).
cnf(s4116,plain,
( spl55_20
| spl55_53
| spl55_84
| ~ spl55_94
| spl55_1896
| spl55_1902
| spl55_2112 ),
inference(sat_conversion,[],[f61820]) ).
cnf(s4138,plain,
( spl55_21
| spl55_45
| ~ spl55_1902 ),
inference(sat_conversion,[],[f61993]) ).
cnf(s4266,plain,
( ~ spl55_130
| ~ spl55_442
| ~ spl55_1959
| ~ spl55_2423 ),
inference(sat_conversion,[],[f63512]) ).
cnf(s4267,plain,
( spl55_44
| spl55_2423
| spl55_2430
| ~ spl55_2548 ),
inference(sat_conversion,[],[f63516]) ).
cnf(s4270,plain,
( spl55_46
| ~ spl55_2430 ),
inference(sat_conversion,[],[f63536]) ).
cnf(s4279,plain,
( ~ spl55_45
| ~ spl55_2311 ),
inference(sat_conversion,[],[f63611]) ).
cnf(s4293,plain,
( ~ spl55_44
| ~ spl55_153 ),
inference(sat_conversion,[],[f63978]) ).
cnf(s4319,plain,
( spl55_21
| spl55_45
| ~ spl55_2062 ),
inference(sat_conversion,[],[f64117]) ).
cnf(s4329,plain,
( ~ spl55_153
| spl55_2548 ),
inference(sat_conversion,[],[f64138]) ).
cnf(s4348,plain,
( spl55_44
| spl55_442
| spl55_2424
| ~ spl55_2548 ),
inference(sat_conversion,[],[f64462]) ).
cnf(s4351,plain,
( ~ spl55_153
| ~ spl55_2424 ),
inference(sat_conversion,[],[f64498]) ).
cnf(s4358,plain,
( ~ spl55_84
| spl55_2549 ),
inference(sat_conversion,[],[f64655]) ).
cnf(s4365,plain,
~ spl55_66,
inference(rat,[],[s3400,s3393]) ).
cnf(s4466,plain,
( spl55_20
| spl55_126 ),
inference(rat,[],[s178,s862]) ).
cnf(s4531,plain,
( spl55_20
| spl55_39
| spl55_94 ),
inference(rat,[],[s126,s173]) ).
cnf(s4563,plain,
spl55_1959,
inference(rat,[],[s2901,s64]) ).
cnf(s4626,plain,
spl55_65,
inference(rat,[],[s58,s4365,s64]) ).
cnf(s4627,plain,
spl55_2064,
inference(rat,[],[s3042,s64,s4626]) ).
cnf(s4632,plain,
~ spl55_20,
inference(rat,[],[s46,s77]) ).
cnf(s4645,plain,
spl55_126,
inference(rat,[],[s4466,s4632]) ).
cnf(s4646,plain,
spl55_94,
inference(rat,[],[s4531,s77,s4632]) ).
cnf(s4648,plain,
spl55_1918,
inference(rat,[],[s2643,s4632,s4645]) ).
cnf(s4649,plain,
spl55_152,
inference(rat,[],[s214,s173,s4645]) ).
cnf(s4653,plain,
~ spl55_1878,
inference(rat,[],[s2756,s2753,s4648]) ).
cnf(s4654,plain,
spl55_1894,
inference(rat,[],[s2644,s4632,s4649]) ).
cnf(s4658,plain,
~ spl55_1896,
inference(rat,[],[s2596,s4646,s4632,s173,s4653]) ).
cnf(s4736,plain,
spl55_45,
inference(rat,[],[s4057,s4116,s4358,s4027,s4092,s3077,s4017,s4021,s4138,s4319,s4632,s173,s4646,s4658,s4654,s40]) ).
cnf(s4737,plain,
~ spl55_2311,
inference(rat,[],[s4279,s4736]) ).
cnf(s4738,plain,
spl55_2062,
inference(rat,[],[s4016,s4627,s4736]) ).
cnf(s4740,plain,
spl55_574,
inference(rat,[],[s4002,s40,s4738]) ).
cnf(s4741,plain,
spl55_153,
inference(rat,[],[s4001,s40,s4738]) ).
cnf(s4746,plain,
~ spl55_129,
inference(rat,[],[s801,s4740]) ).
cnf(s4748,plain,
~ spl55_2424,
inference(rat,[],[s4351,s4741]) ).
cnf(s4749,plain,
spl55_2548,
inference(rat,[],[s4329,s4741]) ).
cnf(s4751,plain,
~ spl55_44,
inference(rat,[],[s4293,s4741]) ).
cnf(s4770,plain,
spl55_442,
inference(rat,[],[s4348,s4748,s4751,s4749]) ).
cnf(s4772,plain,
spl55_130,
inference(rat,[],[s4092,s4746,s4749]) ).
cnf(s4836,plain,
~ spl55_46,
inference(rat,[],[s3792,s4737,s4751,s4770]) ).
cnf(s4839,plain,
~ spl55_2423,
inference(rat,[],[s4266,s4770,s4563,s4772]) ).
cnf(s4848,plain,
~ spl55_2430,
inference(rat,[],[s4270,s4836]) ).
cnf(s4852,plain,
$false,
inference(rat,[],[s4267,s4749,s4751,s4848,s4839]) ).
fof(f64785,plain,
$false,
inference(avatar_sat_refutation,[],[s4852]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO329+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n008.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 08:06:54 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.70/2.88 % (907761)Detected formulas, will run a generic FOF schedule.
% 13.70/2.88 % (907768)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=2824986993:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.70/2.88 % (907772)dis-21_1_sil=8000:lcm=predicate:random_seed=2155767975: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)
% 13.70/2.88 % (907771)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3351501632:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.70/2.88 % (907770)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3075507069:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.70/2.88 % (907769)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1374832498:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.70/2.88 % (907767)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=2436962454:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.70/2.88 % (907766)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=151322710:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.70/2.88 % (907769)Instruction limit reached!
% 13.70/2.88 % (907769)------------------------------
% 13.70/2.88 % (907769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.88 % (907769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.88 % (907769)CaDiCaL version: 2.1.3
% 13.70/2.88 % (907769)Termination reason: Instruction limit
% 13.70/2.88 % (907769)Termination phase: Saturation
% 13.70/2.88 % (907769)Time elapsed: 0.058 s
% 13.70/2.88 % (907769)Peak memory usage: 89 MB
% 13.70/2.88 % (907769)Instructions burned: 110 (million)
% 13.70/2.88 % (907770)Instruction limit reached!
% 13.70/2.88 % (907770)------------------------------
% 13.70/2.88 % (907770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.88 % (907770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.88 % (907770)CaDiCaL version: 2.1.3
% 13.70/2.88 % (907770)Termination reason: Instruction limit
% 13.70/2.88 % (907770)Termination phase: Saturation
% 13.70/2.88 % (907770)Time elapsed: 0.059 s
% 13.70/2.88 % (907770)Peak memory usage: 88 MB
% 13.70/2.88 % (907770)Instructions burned: 120 (million)
% 13.70/2.88 % (907772)Instruction limit reached!
% 13.70/2.88 % (907772)------------------------------
% 13.70/2.88 % (907772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.88 % (907772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.88 % (907772)CaDiCaL version: 2.1.3
% 13.70/2.88 % (907772)Termination reason: Instruction limit
% 13.70/2.88 % (907772)Termination phase: Saturation
% 13.70/2.88 % (907772)Time elapsed: 0.069 s
% 13.70/2.88 % (907772)Peak memory usage: 90 MB
% 13.70/2.88 % (907772)Instructions burned: 129 (million)
% 13.70/2.88 % (907771)Instruction limit reached!
% 13.70/2.88 % (907771)------------------------------
% 13.70/2.88 % (907771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.88 % (907771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.88 % (907771)CaDiCaL version: 2.1.3
% 13.70/2.88 % (907771)Termination reason: Instruction limit
% 13.70/2.88 % (907771)Termination phase: Saturation
% 13.70/2.88 % (907771)Time elapsed: 0.085 s
% 13.70/2.88 % (907771)Peak memory usage: 90 MB
% 13.70/2.88 % (907771)Instructions burned: 141 (million)
% 13.70/2.88 % (907781)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1817878098:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.70/2.88 % (907780)lrs+10_1_sil=8000:sp=occurrence:random_seed=2663861838:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 13.70/2.88 % (907783)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=2096422601:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 13.70/2.88 % (907782)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4151534475:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.70/2.88 % (907781)Instruction limit reached!
% 13.70/2.88 % (907781)------------------------------
% 13.70/2.88 % (907781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.62/3.84 % (907781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.62/3.84 % (907781)CaDiCaL version: 2.1.3
% 20.62/3.84 % (907781)Termination reason: Instruction limit
% 20.62/3.84 % (907781)Termination phase: Saturation
% 20.62/3.84 % (907781)Time elapsed: 0.078 s
% 20.62/3.84 % (907781)Peak memory usage: 89 MB
% 20.62/3.84 % (907781)Instructions burned: 158 (million)
% 20.62/3.84 % (907783)Instruction limit reached!
% 20.62/3.84 % (907783)------------------------------
% 20.62/3.84 % (907783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.62/3.84 % (907783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.62/3.84 % (907783)CaDiCaL version: 2.1.3
% 20.62/3.84 % (907783)Termination reason: Instruction limit
% 20.62/3.84 % (907783)Termination phase: Saturation
% 20.62/3.84 % (907783)Time elapsed: 0.115 s
% 20.62/3.84 % (907783)Peak memory usage: 90 MB
% 20.62/3.84 % (907783)Instructions burned: 250 (million)
% 20.62/3.84 % (907780)Instruction limit reached!
% 20.62/3.84 % (907780)------------------------------
% 20.62/3.84 % (907780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.62/3.84 % (907780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.62/3.84 % (907780)CaDiCaL version: 2.1.3
% 20.62/3.84 % (907780)Termination reason: Instruction limit
% 20.62/3.84 % (907780)Termination phase: Saturation
% 20.62/3.84 % (907780)Time elapsed: 0.156 s
% 20.62/3.84 % (907780)Peak memory usage: 92 MB
% 20.62/3.84 % (907780)Instructions burned: 286 (million)
% 20.62/3.84 % (907782)Instruction limit reached!
% 20.62/3.84 % (907782)------------------------------
% 20.62/3.84 % (907782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.62/3.84 % (907782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.62/3.84 % (907782)CaDiCaL version: 2.1.3
% 20.62/3.84 % (907782)Termination reason: Instruction limit
% 20.62/3.84 % (907782)Termination phase: Saturation
% 20.62/3.84 % (907782)Time elapsed: 0.185 s
% 20.62/3.84 % (907782)Peak memory usage: 91 MB
% 20.62/3.84 % (907782)Instructions burned: 326 (million)
% 20.62/3.84 % (907788)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4151454780:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 20.62/3.84 % (907789)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3690829737:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 20.62/3.84 % (907790)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3914660648:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 20.62/3.84 % (907791)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3463695526:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 20.62/3.84 % (907790)Instruction limit reached!
% 20.62/3.84 % (907790)------------------------------
% 20.62/3.84 % (907790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.62/3.84 % (907790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.62/3.84 % (907790)CaDiCaL version: 2.1.3
% 20.62/3.84 % (907790)Termination reason: Instruction limit
% 20.62/3.84 % (907790)Termination phase: Saturation
% 20.62/3.84 % (907790)Time elapsed: 0.059 s
% 20.62/3.84 % (907790)Peak memory usage: 89 MB
% 20.62/3.84 % (907790)Instructions burned: 114 (million)
% 20.62/3.84 % (907788)Instruction limit reached!
% 20.62/3.84 % (907788)------------------------------
% 20.62/3.84 % (907788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.62/3.84 % (907788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.62/3.84 % (907788)CaDiCaL version: 2.1.3
% 20.62/3.84 % (907788)Termination reason: Instruction limit
% 20.62/3.84 % (907788)Termination phase: Saturation
% 20.62/3.84 % (907788)Time elapsed: 0.140 s
% 20.62/3.84 % (907788)Peak memory usage: 89 MB
% 20.62/3.84 % (907788)Instructions burned: 294 (million)
% 20.62/3.84 % (907791)Refutation not found, incomplete strategy
% 20.62/3.84 % (907791)------------------------------
% 20.62/3.84 % (907791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.62/3.84 % (907791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.62/3.84 % (907791)CaDiCaL version: 2.1.3
% 20.62/3.84 % (907791)Termination reason: Refutation not found, incomplete strategy
% 20.62/3.84 % (907791)Time elapsed: 0.031 s
% 20.62/3.84 % (907791)Peak memory usage: 89 MB
% 20.62/3.84 % (907791)Instructions burned: 63 (million)
% 41.48/6.78 % (907796)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1609258743:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 41.48/6.78 % (907797)lrs+10_1_sil=8000:sp=occurrence:random_seed=2203962160:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 41.48/6.78 % (907796)Instruction limit reached!
% 41.48/6.78 % (907796)------------------------------
% 41.48/6.78 % (907796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.48/6.78 % (907796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.48/6.78 % (907796)CaDiCaL version: 2.1.3
% 41.48/6.78 % (907796)Termination reason: Instruction limit
% 41.48/6.78 % (907796)Termination phase: Saturation
% 41.48/6.78 % (907796)Time elapsed: 0.053 s
% 41.48/6.78 % (907796)Peak memory usage: 88 MB
% 41.48/6.78 % (907796)Instructions burned: 116 (million)
% 41.48/6.78 % (907791)------------------------------
% 41.48/6.78 % (907791)------------------------------
% 41.48/6.78 % (907800)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4207792615:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 41.48/6.78 % (907800)Refutation not found, incomplete strategy
% 41.48/6.78 % (907800)------------------------------
% 41.48/6.78 % (907800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.48/6.78 % (907800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.48/6.78 % (907800)CaDiCaL version: 2.1.3
% 41.48/6.78 % (907800)Termination reason: Refutation not found, incomplete strategy
% 41.48/6.78 % (907800)Time elapsed: 0.019 s
% 41.48/6.78 % (907800)Peak memory usage: 89 MB
% 41.48/6.78 % (907800)Instructions burned: 36 (million)
% 41.48/6.78 % (907801)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=351900460:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 41.48/6.78 % (907800)------------------------------
% 41.48/6.78 % (907800)------------------------------
% 41.48/6.78 % (907797)Instruction limit reached!
% 41.48/6.78 % (907797)------------------------------
% 41.48/6.78 % (907797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.48/6.78 % (907797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.48/6.78 % (907797)CaDiCaL version: 2.1.3
% 41.48/6.78 % (907797)Termination reason: Instruction limit
% 41.48/6.78 % (907797)Termination phase: Saturation
% 41.48/6.78 % (907797)Time elapsed: 0.490 s
% 41.48/6.78 % (907797)Peak memory usage: 100 MB
% 41.48/6.78 % (907797)Instructions burned: 907 (million)
% 41.48/6.78 % (907804)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2266095649:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 41.48/6.78 % (907805)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2467697135:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 41.48/6.78 % (907804)Instruction limit reached!
% 41.48/6.78 % (907804)------------------------------
% 41.48/6.78 % (907804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.48/6.78 % (907804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.48/6.78 % (907804)CaDiCaL version: 2.1.3
% 41.48/6.78 % (907804)Termination reason: Instruction limit
% 41.48/6.78 % (907804)Termination phase: Saturation
% 41.48/6.78 % (907804)Time elapsed: 0.067 s
% 41.48/6.78 % (907804)Peak memory usage: 93 MB
% 41.48/6.78 % (907804)Instructions burned: 136 (million)
% 41.48/6.78 % (907808)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3669603673:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 41.48/6.78 % (907805)Instruction limit reached!
% 41.48/6.78 % (907805)------------------------------
% 41.48/6.78 % (907805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.48/6.78 % (907805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.48/6.78 % (907805)CaDiCaL version: 2.1.3
% 41.48/6.78 % (907805)Termination reason: Instruction limit
% 41.48/6.78 % (907805)Termination phase: Saturation
% 41.48/6.78 % (907805)Time elapsed: 0.280 s
% 41.48/6.78 % (907805)Peak memory usage: 92 MB
% 41.48/6.78 % (907805)Instructions burned: 592 (million)
% 41.48/6.78 % (907810)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=3345527540:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 50.69/9.17 % (907810)Instruction limit reached!
% 50.69/9.17 % (907810)------------------------------
% 50.69/9.17 % (907810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907810)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907810)Termination reason: Instruction limit
% 50.69/9.17 % (907810)Termination phase: Saturation
% 50.69/9.17 % (907810)Time elapsed: 0.067 s
% 50.69/9.17 % (907810)Peak memory usage: 90 MB
% 50.69/9.17 % (907810)Instructions burned: 125 (million)
% 50.69/9.17 % (907789)Instruction limit reached!
% 50.69/9.17 % (907789)------------------------------
% 50.69/9.17 % (907789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907789)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907789)Termination reason: Instruction limit
% 50.69/9.17 % (907789)Termination phase: Saturation
% 50.69/9.17 % (907789)Time elapsed: 1.473 s
% 50.69/9.17 % (907789)Peak memory usage: 141 MB
% 50.69/9.17 % (907789)Instructions burned: 2351 (million)
% 50.69/9.17 % (907812)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1042738437:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi)
% 50.69/9.17 % (907813)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4150097196:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 50.69/9.17 % (907812)Instruction limit reached!
% 50.69/9.17 % (907812)------------------------------
% 50.69/9.17 % (907812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907812)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907812)Termination reason: Instruction limit
% 50.69/9.17 % (907812)Termination phase: Saturation
% 50.69/9.17 % (907812)Time elapsed: 0.078 s
% 50.69/9.17 % (907812)Peak memory usage: 91 MB
% 50.69/9.17 % (907812)Instructions burned: 135 (million)
% 50.69/9.17 % (907813)Refutation not found, incomplete strategy
% 50.69/9.17 % (907813)------------------------------
% 50.69/9.17 % (907813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907813)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907813)Termination reason: Refutation not found, incomplete strategy
% 50.69/9.17 % (907813)Time elapsed: 0.005 s
% 50.69/9.17 % (907813)Peak memory usage: 89 MB
% 50.69/9.17 % (907813)Instructions burned: 7 (million)
% 50.69/9.17 % (907816)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=429043228:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 50.69/9.17 % (907816)Refutation not found, incomplete strategy
% 50.69/9.17 % (907816)------------------------------
% 50.69/9.17 % (907816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907816)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907816)Termination reason: Refutation not found, incomplete strategy
% 50.69/9.17 % (907816)Time elapsed: 0.009 s
% 50.69/9.17 % (907816)Peak memory usage: 89 MB
% 50.69/9.17 % (907816)Instructions burned: 15 (million)
% 50.69/9.17 % (907813)------------------------------
% 50.69/9.17 % (907813)------------------------------
% 50.69/9.17 % (907816)------------------------------
% 50.69/9.17 % (907816)------------------------------
% 50.69/9.17 % (907818)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=1508206431:i=6060:aac=none:ins=25_2974 on theBenchmark for (2974ds/6060Mi)
% 50.69/9.17 % (907820)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=4148646845:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 50.69/9.17 % (907820)Instruction limit reached!
% 50.69/9.17 % (907820)------------------------------
% 50.69/9.17 % (907820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907820)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907820)Termination reason: Instruction limit
% 50.69/9.17 % (907820)Termination phase: Saturation
% 50.69/9.17 % (907820)Time elapsed: 0.077 s
% 50.69/9.17 % (907820)Peak memory usage: 92 MB
% 50.69/9.17 % (907820)Instructions burned: 151 (million)
% 50.69/9.17 % (907822)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3573375084:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 50.69/9.17 % (907801)Instruction limit reached!
% 50.69/9.17 % (907801)------------------------------
% 50.69/9.17 % (907801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907801)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907801)Termination reason: Instruction limit
% 50.69/9.17 % (907801)Termination phase: Saturation
% 50.69/9.17 % (907801)Time elapsed: 2.981 s
% 50.69/9.17 % (907801)Peak memory usage: 153 MB
% 50.69/9.17 % (907801)Instructions burned: 5203 (million)
% 50.69/9.17 % (907824)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=178003966:i=667:av=off:fsr=off_2958 on theBenchmark for (2958ds/667Mi)
% 50.69/9.17 % (907824)Refutation not found, incomplete strategy
% 50.69/9.17 % (907824)------------------------------
% 50.69/9.17 % (907824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907824)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907824)Termination reason: Refutation not found, incomplete strategy
% 50.69/9.17 % (907824)Time elapsed: 0.024 s
% 50.69/9.17 % (907824)Peak memory usage: 90 MB
% 50.69/9.17 % (907824)Instructions burned: 49 (million)
% 50.69/9.17 % (907824)------------------------------
% 50.69/9.17 % (907824)------------------------------
% 50.69/9.17 % (907826)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=799016097:s2a=on:i=185:s2at=1.8:fdi=4_2953 on theBenchmark for (2953ds/185Mi)
% 50.69/9.17 % (907826)Instruction limit reached!
% 50.69/9.17 % (907826)------------------------------
% 50.69/9.17 % (907826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907826)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907826)Termination reason: Instruction limit
% 50.69/9.17 % (907826)Termination phase: Saturation
% 50.69/9.17 % (907826)Time elapsed: 0.096 s
% 50.69/9.17 % (907826)Peak memory usage: 93 MB
% 50.69/9.17 % (907826)Instructions burned: 186 (million)
% 50.69/9.17 % (907828)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1287312358:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2951 on theBenchmark for (2951ds/193Mi)
% 50.69/9.17 % (907828)Instruction limit reached!
% 50.69/9.17 % (907828)------------------------------
% 50.69/9.17 % (907828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907828)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907828)Termination reason: Instruction limit
% 50.69/9.17 % (907828)Termination phase: Saturation
% 50.69/9.17 % (907828)Time elapsed: 0.106 s
% 50.69/9.17 % (907828)Peak memory usage: 91 MB
% 50.69/9.17 % (907828)Instructions burned: 194 (million)
% 50.69/9.17 % (907830)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1452972982:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2948 on theBenchmark for (2948ds/4850Mi)
% 50.69/9.17 % (907830)Refutation not found, incomplete strategy
% 50.69/9.17 % (907830)------------------------------
% 50.69/9.17 % (907830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907830)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907830)Termination reason: Refutation not found, incomplete strategy
% 50.69/9.17 % (907830)Time elapsed: 0.018 s
% 50.69/9.17 % (907830)Peak memory usage: 89 MB
% 50.69/9.17 % (907830)Instructions burned: 34 (million)
% 50.69/9.17 % (907830)------------------------------
% 50.69/9.17 % (907830)------------------------------
% 50.69/9.17 % (907832)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1280113343:i=12111:sd=1:ss=included_2944 on theBenchmark for (2944ds/12111Mi)
% 50.69/9.17 % (907818)Instruction limit reached!
% 50.69/9.17 % (907818)------------------------------
% 50.69/9.17 % (907818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907818)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907818)Termination reason: Instruction limit
% 50.69/9.17 % (907818)Termination phase: Saturation
% 50.69/9.17 % (907818)Time elapsed: 3.175 s
% 50.69/9.17 % (907818)Peak memory usage: 143 MB
% 50.69/9.17 % (907818)Instructions burned: 6062 (million)
% 50.69/9.17 % (907834)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2405181075:i=319:kws=precedence:fsr=off_2940 on theBenchmark for (2940ds/319Mi)
% 50.69/9.17 % (907834)Instruction limit reached!
% 50.69/9.17 % (907834)------------------------------
% 50.69/9.17 % (907834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907834)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907834)Termination reason: Instruction limit
% 50.69/9.17 % (907834)Termination phase: Saturation
% 50.69/9.17 % (907834)Time elapsed: 0.161 s
% 50.69/9.17 % (907834)Peak memory usage: 94 MB
% 50.69/9.17 % (907834)Instructions burned: 320 (million)
% 50.69/9.17 % (907836)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3309970606:i=2064:ep=RST_2937 on theBenchmark for (2937ds/2064Mi)
% 50.69/9.17 % (907836)Instruction limit reached!
% 50.69/9.17 % (907836)------------------------------
% 50.69/9.17 % (907836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.69/9.17 % (907836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.69/9.17 % (907836)CaDiCaL version: 2.1.3
% 50.69/9.17 % (907836)Termination reason: Instruction limit
% 50.69/9.17 % (907836)Termination phase: Saturation
% 50.69/9.17 % (907836)Time elapsed: 0.974 s
% 50.69/9.17 % (907836)Peak memory usage: 96 MB
% 50.69/9.17 % (907836)Instructions burned: 2064 (million)
% 50.69/9.17 % (907838)dis-1011_128_sil=32000:random_seed=518881676:i=3706:ep=RST:av=off_2925 on theBenchmark for (2925ds/3706Mi)
% 50.69/9.17 % (907767)First to succeed.
% 50.69/9.17 % (907767)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-907761"
% 50.69/9.17 % (907767)Refutation found. Thanks to Tanya!
% 50.69/9.17 % SZS status Theorem for theBenchmark
% 50.69/9.17 % SZS output start Proof for theBenchmark
% See solution above
% 59.30/9.27 % (907767)------------------------------
% 59.30/9.27 % (907767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.30/9.27 % (907767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.30/9.27 % (907767)CaDiCaL version: 2.1.3
% 59.30/9.27 % (907767)Termination reason: Refutation
% 59.30/9.27 % (907767)Time elapsed: 7.830 s
% 59.30/9.27 % (907767)Peak memory usage: 186 MB
% 59.30/9.27 % (907767)Instructions burned: 13032 (million)
% 59.30/9.27 % (907767)------------------------------
% 59.30/9.27 % (907767)------------------------------
% 59.30/9.27 % (907761)Success in time 8.312 s
% 59.30/9.27 % Vampire exiting
%------------------------------------------------------------------------------