%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO330+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 : n011.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:29 AM UTC 2026
% Result : Theorem 30.74s 5.19s
% Output : Refutation 31.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 26
% Syntax : Number of formulae : 307 ( 56 unt; 8 def)
% Number of atoms : 1908 ( 576 equ)
% Maximal formula atoms : 26 ( 6 avg)
% Number of connectives : 2801 (1200 ~;1441 |; 136 &)
% ( 14 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 9 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 9 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-3 aty)
% Number of variables : 681 ( 0 sgn 651 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vangle(vd1287,vd1289,vd1288) = vangle(vd1287,vd1288,vd1289),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(380, 1351, 0)') ).
fof(f2,negated_conjecture,
vangle(vd1287,vd1289,vd1288) != vangle(vd1287,vd1288,vd1289),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f15,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(f18,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(f33,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(f41,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(f43,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(f45,axiom,
! [X0,X1] :
( ( X0 != X1
& ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ? [X4] :
( ron(X1,X4)
& ron(X0,X4)
& rline(X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(51), 0), imp(cond(axiom(51), 0)))') ).
fof(f47,axiom,
ron(vd1288,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(s3(plural(370)), 0)') ).
fof(f56,axiom,
ron(vd1289,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct2(369), 0)') ).
fof(f92,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(f99,axiom,
! [X0,X1,X2,X3] :
( ( rinside(X0,X2)
& X2 = X3
& rcircle(X3)
& X0 = X1
& rpoint(X1) )
=> ~ ron(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(79), 0), imp(cond(axiom(79), 0)))') ).
fof(f102,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(f105,axiom,
ron(vd1287,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(s2(plural(369)), 0)') ).
fof(f111,axiom,
rline(vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(347, 0)') ).
fof(f112,axiom,
ron(vd1287,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(s1(plural(346)), 0)') ).
fof(f113,axiom,
rline(vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(346, 0)') ).
fof(f134,axiom,
! [X0,X1,X2,X3,X4] :
( ( rR(X2,X0,X1)
& ~ rinside(X2,X3)
& ( ron(X0,X3)
| rinside(X0,X3) )
& X3 = X4
& rcircle(X4)
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ( ~ ron(X1,X3)
& ~ ron(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(123), 0), imp(cond(axiom(123), 0)))') ).
fof(f148,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(f190,plain,
vangle(vd1287,vd1289,vd1288) != vangle(vd1287,vd1288,vd1289),
inference(flattening,[],[f2]) ).
fof(f211,plain,
! [X0,X1] :
( ? [X4] :
( ron(X1,X4)
& ron(X0,X4)
& rline(X4) )
| X0 = X1
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f45]) ).
fof(f212,plain,
! [X0,X1] :
( ? [X4] :
( ron(X1,X4)
& ron(X0,X4)
& rline(X4) )
| X0 = X1
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f211]) ).
fof(f242,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,[],[f15]) ).
fof(f243,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,[],[f242]) ).
fof(f272,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,[],[f41]) ).
fof(f273,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,[],[f272]) ).
fof(f316,plain,
! [X0,X1,X2,X3,X4] :
( ( ~ ron(X1,X3)
& ~ ron(X1,X3) )
| ~ rR(X2,X0,X1)
| rinside(X2,X3)
| ( ~ ron(X0,X3)
& ~ rinside(X0,X3) )
| X3 != X4
| ~ rcircle(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f134]) ).
fof(f317,plain,
! [X0,X1,X2,X3,X4] :
( ( ~ ron(X1,X3)
& ~ ron(X1,X3) )
| ~ rR(X2,X0,X1)
| rinside(X2,X3)
| ( ~ ron(X0,X3)
& ~ rinside(X0,X3) )
| X3 != X4
| ~ rcircle(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f316]) ).
fof(f352,plain,
! [X0,X1] :
( rinside(X0,X1)
| ~ rcenter(X0,X1) ),
inference(ennf_transformation,[],[f148]) ).
fof(f355,plain,
! [X0,X1,X2,X3] :
( ~ ron(X0,X2)
| ~ rinside(X0,X2)
| X2 != X3
| ~ rcircle(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(ennf_transformation,[],[f99]) ).
fof(f356,plain,
! [X0,X1,X2,X3] :
( ~ ron(X0,X2)
| ~ rinside(X0,X2)
| X2 != X3
| ~ rcircle(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(flattening,[],[f355]) ).
fof(f378,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,[],[f102]) ).
fof(f379,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,[],[f378]) ).
fof(f404,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,[],[f18]) ).
fof(f405,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,[],[f404]) ).
fof(f406,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,[],[f92]) ).
fof(f407,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,[],[f406]) ).
fof(f408,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,[],[f43]) ).
fof(f409,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,[],[f408]) ).
fof(f426,plain,
! [X0,X1] :
( ? [X2] :
( ron(X1,X2)
& ron(X0,X2)
& rline(X2) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(rectify,[],[f212]) ).
fof(f427,plain,
! [X0,X1] :
( ( ron(X1,sK9(X0,X1))
& ron(X0,sK9(X0,X1))
& rline(sK9(X0,X1)) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X2,sK9(X0,X1))],[f426]) ).
fof(f428,plain,
( vf(vd1287,vd1288) = vf(vd1287,vd1289)
& vd1288 != vd1289
& vd1287 != vd1289
& vd1287 != vd1288
& vd1289 = sK10
& rpoint(sK10)
& vd1288 = sK11
& rpoint(sK11)
& vd1287 = sK12
& rpoint(sK12) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12]),skolemize(X0,sK10),skolemize(X1,sK11),skolemize(X2,sK12)],[f33]) ).
fof(f473,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,[],[f379]) ).
fof(f474,plain,
! [X0,X1] :
( ( ron(X1,sK46(X0,X1))
& rcenter(X0,sK46(X0,X1))
& rcircle(sK46(X0,X1)) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46]),skolemize(X2,sK46(X0,X1))],[f473]) ).
fof(f483,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,[],[f405]) ).
fof(f484,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,[],[f483]) ).
fof(f485,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,[],[f409]) ).
fof(f487,plain,
vangle(vd1287,vd1289,vd1288) != vangle(vd1287,vd1288,vd1289),
inference(cnf_transformation,[],[f190]) ).
fof(f517,plain,
! [X3,X0,X1,X4] :
( rline(sK9(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f427]) ).
fof(f518,plain,
! [X3,X0,X1,X4] :
( ron(X0,sK9(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f427]) ).
fof(f519,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK9(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f427]) ).
fof(f551,plain,
rpoint(sK12),
inference(cnf_transformation,[],[f428]) ).
fof(f552,plain,
vd1287 = sK12,
inference(cnf_transformation,[],[f428]) ).
fof(f553,plain,
rpoint(sK11),
inference(cnf_transformation,[],[f428]) ).
fof(f554,plain,
vd1288 = sK11,
inference(cnf_transformation,[],[f428]) ).
fof(f555,plain,
rpoint(sK10),
inference(cnf_transformation,[],[f428]) ).
fof(f556,plain,
vd1289 = sK10,
inference(cnf_transformation,[],[f428]) ).
fof(f557,plain,
vd1287 != vd1288,
inference(cnf_transformation,[],[f428]) ).
fof(f558,plain,
vd1287 != vd1289,
inference(cnf_transformation,[],[f428]) ).
fof(f559,plain,
vd1289 != vd1288,
inference(cnf_transformation,[],[f428]) ).
fof(f560,plain,
vf(vd1287,vd1288) = vf(vd1287,vd1289),
inference(cnf_transformation,[],[f428]) ).
fof(f578,plain,
ron(vd1288,vd1295),
inference(cnf_transformation,[],[f47]) ).
fof(f596,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,[],[f243]) ).
fof(f631,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,[],[f273]) ).
fof(f633,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,[],[f273]) ).
fof(f674,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ ron(X1,X3)
| ~ rR(X2,X0,X1)
| rinside(X2,X3)
| ~ rinside(X0,X3)
| X3 != X4
| ~ rcircle(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f317]) ).
fof(f695,plain,
rline(vd1295),
inference(cnf_transformation,[],[f113]) ).
fof(f696,plain,
ron(vd1287,vd1295),
inference(cnf_transformation,[],[f112]) ).
fof(f715,plain,
rline(vd1297),
inference(cnf_transformation,[],[f111]) ).
fof(f719,plain,
ron(vd1287,vd1297),
inference(cnf_transformation,[],[f105]) ).
fof(f722,plain,
ron(vd1289,vd1297),
inference(cnf_transformation,[],[f56]) ).
fof(f728,plain,
! [X0,X1] :
( ~ rcenter(X0,X1)
| rinside(X0,X1) ),
inference(cnf_transformation,[],[f352]) ).
fof(f730,plain,
! [X2,X3,X0,X1] :
( ~ ron(X0,X2)
| ~ rinside(X0,X2)
| X2 != X3
| ~ rcircle(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f356]) ).
fof(f763,plain,
! [X3,X0,X1,X4] :
( rcircle(sK46(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f474]) ).
fof(f764,plain,
! [X3,X0,X1,X4] :
( rcenter(X0,sK46(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f474]) ).
fof(f765,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK46(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f474]) ).
fof(f789,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,[],[f484]) ).
fof(f790,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,[],[f484]) ).
fof(f792,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,[],[f407]) ).
fof(f793,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,[],[f485]) ).
fof(f798,plain,
vangle(sK12,sK10,sK11) != vangle(sK12,sK11,sK10),
inference(definition_unfolding,[],[f487,f552,f556,f554,f552,f554,f556]) ).
fof(f830,plain,
vf(sK12,sK11) = vf(sK12,sK10),
inference(definition_unfolding,[],[f560,f552,f554,f552,f556]) ).
fof(f831,plain,
sK10 != sK11,
inference(definition_unfolding,[],[f559,f556,f554]) ).
fof(f832,plain,
sK10 != sK12,
inference(definition_unfolding,[],[f558,f552,f556]) ).
fof(f833,plain,
sK11 != sK12,
inference(definition_unfolding,[],[f557,f552,f554]) ).
fof(f851,plain,
ron(sK11,vd1295),
inference(definition_unfolding,[],[f578,f554]) ).
fof(f855,plain,
ron(sK12,vd1295),
inference(definition_unfolding,[],[f696,f552]) ).
fof(f860,plain,
ron(sK12,vd1297),
inference(definition_unfolding,[],[f719,f552]) ).
fof(f863,plain,
ron(sK10,vd1297),
inference(definition_unfolding,[],[f722,f556]) ).
fof(f946,plain,
! [X3,X0,X4] :
( ron(X3,sK9(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f519]) ).
fof(f947,plain,
! [X3,X4] :
( ron(X3,sK9(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f946]) ).
fof(f948,plain,
! [X3,X0,X4] :
( ron(X0,sK9(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f518]) ).
fof(f949,plain,
! [X3,X4] :
( ron(X4,sK9(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f948]) ).
fof(f950,plain,
! [X3,X0,X4] :
( rline(sK9(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f517]) ).
fof(f951,plain,
! [X3,X4] :
( rline(sK9(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f950]) ).
fof(f989,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,[],[f596]) ).
fof(f990,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,[],[f989]) ).
fof(f991,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,[],[f990]) ).
fof(f992,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,[],[f991]) ).
fof(f993,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,[],[f992]) ).
fof(f994,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,[],[f993]) ).
fof(f995,plain,
! [X10,X11,X8,X9,X7,X12,X13] :
( ~ ron(X13,X8)
| rR(X13,X11,X9)
| rR(X13,X12,X10)
| X9 = X13
| X10 = X13
| X11 = X13
| X12 = X13
| ~ ron(X9,X7)
| ~ ron(X11,X7)
| ~ ron(X10,X8)
| ~ ron(X12,X8)
| vangle(X10,X13,X9) = vangle(X12,X13,X11)
| ~ rline(X7)
| ~ rline(X8)
| ~ rpoint(X9)
| ~ rpoint(X10)
| ~ rpoint(X11)
| ~ rpoint(X12)
| ~ rpoint(X13) ),
inference(equality_resolution,[],[f994]) ).
fof(f1165,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,[],[f633]) ).
fof(f1166,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X3,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1165]) ).
fof(f1167,plain,
! [X3,X4,X5] :
( ~ rR(X4,X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1166]) ).
fof(f1168,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1167]) ).
fof(f1173,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,[],[f631]) ).
fof(f1174,plain,
! [X3,X0,X4,X5] :
( rR(X4,X3,X0)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1173]) ).
fof(f1175,plain,
! [X3,X4,X5] :
( ~ rR(X4,X5,X3)
| rR(X4,X3,X5)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1174]) ).
fof(f1329,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ~ ron(X1,X4)
| ~ rR(X2,X0,X1)
| rinside(X2,X4)
| ~ rinside(X0,X4)
| ~ rcircle(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f674]) ).
fof(f1330,plain,
! [X0,X1,X6,X7,X4,X5] :
( ~ ron(X1,X4)
| ~ rR(X5,X0,X1)
| rinside(X5,X4)
| ~ rinside(X0,X4)
| ~ rcircle(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1329]) ).
fof(f1331,plain,
! [X0,X6,X7,X4,X5] :
( ~ ron(X6,X4)
| ~ rR(X5,X0,X6)
| rinside(X5,X4)
| ~ rinside(X0,X4)
| ~ rcircle(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1330]) ).
fof(f1332,plain,
! [X6,X7,X4,X5] :
( ~ rR(X5,X7,X6)
| ~ ron(X6,X4)
| rinside(X5,X4)
| ~ rinside(X7,X4)
| ~ rcircle(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1331]) ).
fof(f1432,plain,
! [X3,X0,X1] :
( ~ ron(X0,X3)
| ~ rinside(X0,X3)
| ~ rcircle(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f730]) ).
fof(f1433,plain,
! [X3,X1] :
( ~ rinside(X1,X3)
| ~ ron(X1,X3)
| ~ rcircle(X3)
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f1432]) ).
fof(f1495,plain,
! [X3,X0,X4] :
( ron(X3,sK46(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f765]) ).
fof(f1496,plain,
! [X3,X4] :
( ron(X3,sK46(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1495]) ).
fof(f1497,plain,
! [X3,X0,X4] :
( rcenter(X0,sK46(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f764]) ).
fof(f1498,plain,
! [X3,X4] :
( rcenter(X4,sK46(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1497]) ).
fof(f1499,plain,
! [X3,X0,X4] :
( rcircle(sK46(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f763]) ).
fof(f1500,plain,
! [X3,X4] :
( rcircle(sK46(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1499]) ).
fof(f1564,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( ron(X4,X7)
| vangle(X2,X0,X4) != v0
| ~ 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,[],[f790]) ).
fof(f1565,plain,
! [X2,X3,X0,X1,X7,X5] :
( ron(X5,X7)
| v0 != 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,[],[f1564]) ).
fof(f1566,plain,
! [X3,X0,X1,X7,X5] :
( ron(X5,X7)
| v0 != 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,[],[f1565]) ).
fof(f1567,plain,
! [X3,X1,X7,X5] :
( v0 != 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,[],[f1566]) ).
fof(f1568,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( vangle(X2,X0,X4) = v0
| 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,[],[f789]) ).
fof(f1569,plain,
! [X2,X3,X0,X1,X7,X5] :
( v0 = 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,[],[f1568]) ).
fof(f1570,plain,
! [X3,X0,X1,X7,X5] :
( v0 = 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,[],[f1569]) ).
fof(f1571,plain,
! [X3,X1,X7,X5] :
( ~ ron(X5,X7)
| rR(X1,X3,X5)
| v0 = vangle(X3,X1,X5)
| ~ ron(X3,X7)
| ~ ron(X1,X7)
| X1 = X5
| X1 = X3
| ~ rline(X7)
| ~ rpoint(X5)
| ~ rpoint(X3)
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f1570]) ).
fof(f1572,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,[],[f792]) ).
fof(f1573,plain,
! [X2,X3,X6,X4,X5] :
( vf(X2,X5) != vf(X2,X6)
| X3 = X4
| ~ ron(X5,X4)
| ~ ron(X6,X3)
| ~ rcenter(X2,X4)
| ~ rcenter(X2,X3)
| ~ rpoint(X5)
| ~ rpoint(X6) ),
inference(equality_resolution,[],[f1572]) ).
fof(f1576,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,[],[f793]) ).
fof(f1577,plain,
! [X2,X3,X1,X5] :
( vf(X2,X1) != vf(X2,X5)
| ron(X1,X3)
| ~ ron(X5,X3)
| ~ rpoint(X5)
| ~ rcenter(X2,X3)
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f1576]) ).
fof(f1586,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f1168]) ).
fof(f1593,definition,
( spl52_2
<=> ron(sK12,vd1297) ),
introduced(definition,[new_symbols(definition,[spl52_2])],[avatar_definition]) ).
fof(f1595,plain,
( ron(sK12,vd1297)
| ~ spl52_2 ),
inference(avatar_component_clause,[],[f1593]) ).
fof(f1597,plain,
spl52_2,
inference(avatar_split_clause,[],[f860,f1593]) ).
fof(f1623,definition,
( spl52_9
<=> ron(sK12,vd1295) ),
introduced(definition,[new_symbols(definition,[spl52_9])],[avatar_definition]) ).
fof(f1625,plain,
( ron(sK12,vd1295)
| ~ spl52_9 ),
inference(avatar_component_clause,[],[f1623]) ).
fof(f1628,plain,
spl52_9,
inference(avatar_split_clause,[],[f855,f1623]) ).
fof(f1658,definition,
( spl52_15
<=> vangle(sK12,sK10,sK11) = vangle(sK12,sK11,sK10) ),
introduced(definition,[new_symbols(definition,[spl52_15])],[avatar_definition]) ).
fof(f1659,plain,
( vangle(sK12,sK10,sK11) != vangle(sK12,sK11,sK10)
| spl52_15 ),
inference(avatar_component_clause,[],[f1658]) ).
fof(f1754,plain,
~ spl52_15,
inference(avatar_split_clause,[],[f798,f1658]) ).
fof(f1758,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK10,X0,X1)
| rR(sK10,X2,X3)
| sK10 = X1
| sK10 = X3
| sK10 = X0
| sK10 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK10,X1) = vangle(X2,sK10,X0)
| ~ rline(X4)
| ~ rline(vd1297)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK10) ),
inference(resolution,[],[f863,f995]) ).
fof(f1807,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X1)
| v0 = vangle(X3,X2,X1)
| ~ ron(X3,sK9(X1,X0))
| ~ ron(X2,sK9(X1,X0))
| X1 = X2
| X2 = X3
| ~ rline(sK9(X1,X0))
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(resolution,[],[f949,f1571]) ).
fof(f1814,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X1)
| v0 = vangle(X3,X2,X1)
| ~ ron(X3,sK9(X1,X0))
| ~ ron(X2,sK9(X1,X0))
| X1 = X2
| X2 = X3
| ~ rline(sK9(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f1807]) ).
fof(f1818,plain,
! [X2,X3,X0,X1] :
( ~ ron(X3,sK9(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X1)
| v0 = vangle(X3,X2,X1)
| X0 = X1
| ~ ron(X2,sK9(X1,X0))
| X1 = X2
| X2 = X3
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f1814,f951]) ).
fof(f1819,plain,
! [X2,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X1,X1)
| v0 = vangle(X1,X2,X1)
| X0 = X1
| ~ ron(X2,sK9(X1,X0))
| X1 = X2
| X1 = X2
| ~ rpoint(X1)
| ~ rpoint(X2)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f1818,f949]) ).
fof(f1820,plain,
! [X2,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X1,X1)
| v0 = vangle(X1,X2,X1)
| X0 = X1
| ~ ron(X2,sK9(X1,X0))
| X1 = X2
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f1819]) ).
fof(f1821,plain,
! [X2,X0,X1] :
( ~ ron(X2,sK9(X1,X0))
| ~ rpoint(X1)
| v0 = vangle(X1,X2,X1)
| X0 = X1
| ~ rpoint(X0)
| X1 = X2
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f1820,f1586]) ).
fof(f1826,plain,
! [X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rpoint(X1)
| v0 = vangle(X1,X0,X1)
| X0 = X1
| ~ rpoint(X0)
| X0 = X1
| ~ rpoint(X0) ),
inference(resolution,[],[f947,f1821]) ).
fof(f1829,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X0)
| v0 = vangle(X3,X2,X0)
| ~ ron(X3,sK9(X1,X0))
| ~ ron(X2,sK9(X1,X0))
| X0 = X2
| X2 = X3
| ~ rline(sK9(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(resolution,[],[f947,f1571]) ).
fof(f1836,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X0)
| v0 = vangle(X3,X2,X0)
| ~ ron(X3,sK9(X1,X0))
| ~ ron(X2,sK9(X1,X0))
| X0 = X2
| X2 = X3
| ~ rline(sK9(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f1829]) ).
fof(f1839,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X1
| v0 = vangle(X1,X0,X1) ),
inference(duplicate_literal_removal,[],[f1826]) ).
fof(f1843,plain,
! [X2,X3,X0,X1] :
( ~ ron(X3,sK9(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X0)
| v0 = vangle(X3,X2,X0)
| X0 = X1
| ~ ron(X2,sK9(X1,X0))
| X0 = X2
| X2 = X3
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f1836,f951]) ).
fof(f1847,plain,
! [X0] :
( ~ rpoint(X0)
| sK12 = X0
| v0 = vangle(sK12,X0,sK12) ),
inference(resolution,[],[f1839,f551]) ).
fof(f1848,plain,
! [X2,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X1,X0)
| v0 = vangle(X1,X2,X0)
| X0 = X1
| ~ ron(X2,sK9(X1,X0))
| X0 = X2
| X1 = X2
| ~ rpoint(X1)
| ~ rpoint(X2)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f1843,f949]) ).
fof(f1851,plain,
! [X2,X0,X1] :
( ~ ron(X2,sK9(X1,X0))
| ~ rpoint(X1)
| rR(X2,X1,X0)
| v0 = vangle(X1,X2,X0)
| X0 = X1
| ~ rpoint(X0)
| X0 = X2
| X1 = X2
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f1848]) ).
fof(f2010,plain,
( sK10 = sK12
| v0 = vangle(sK12,sK10,sK12) ),
inference(resolution,[],[f1847,f555]) ).
fof(f2014,plain,
v0 = vangle(sK12,sK10,sK12),
inference(forward_subsumption_resolution,[],[f2010,f832]) ).
fof(f2112,plain,
! [X0,X1] :
( rinside(X0,sK46(X0,X1))
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f728,f1498]) ).
fof(f2175,plain,
! [X2,X0,X1] :
( vf(sK12,sK10) != vf(sK12,X0)
| X1 = X2
| ~ ron(X0,X2)
| ~ ron(sK11,X1)
| ~ rcenter(sK12,X2)
| ~ rcenter(sK12,X1)
| ~ rpoint(X0)
| ~ rpoint(sK11) ),
inference(superposition,[],[f1573,f830]) ).
fof(f2186,plain,
! [X2,X0,X1] :
( vf(sK12,sK10) != vf(sK12,X0)
| X1 = X2
| ~ ron(X0,X2)
| ~ ron(sK11,X1)
| ~ rcenter(sK12,X2)
| ~ rcenter(sK12,X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2175,f553]) ).
fof(f2236,plain,
! [X0,X1] :
( X0 = X1
| ~ ron(sK10,X1)
| ~ ron(sK11,X0)
| ~ rcenter(sK12,X1)
| ~ rcenter(sK12,X0)
| ~ rpoint(sK10) ),
inference(equality_resolution,[],[f2186]) ).
fof(f2238,plain,
! [X0,X1] :
( ~ rcenter(sK12,X1)
| ~ ron(sK10,X1)
| ~ ron(sK11,X0)
| X0 = X1
| ~ rcenter(sK12,X0) ),
inference(forward_subsumption_resolution,[],[f2236,f555]) ).
fof(f2249,plain,
! [X0,X1] :
( ~ ron(sK10,sK46(sK12,X0))
| ~ ron(sK11,X1)
| sK46(sK12,X0) = X1
| ~ rcenter(sK12,X1)
| sK12 = X0
| ~ rpoint(X0)
| ~ rpoint(sK12) ),
inference(resolution,[],[f2238,f1498]) ).
fof(f2250,plain,
! [X0,X1] :
( ~ ron(sK10,sK46(sK12,X0))
| ~ ron(sK11,X1)
| sK46(sK12,X0) = X1
| ~ rcenter(sK12,X1)
| sK12 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2249,f551]) ).
fof(f2251,plain,
! [X0] :
( ~ ron(sK11,X0)
| sK46(sK12,sK10) = X0
| ~ rcenter(sK12,X0)
| sK10 = sK12
| ~ rpoint(sK10)
| sK10 = sK12
| ~ rpoint(sK10)
| ~ rpoint(sK12) ),
inference(resolution,[],[f2250,f1496]) ).
fof(f2252,plain,
! [X0] :
( ~ ron(sK11,X0)
| sK46(sK12,sK10) = X0
| ~ rcenter(sK12,X0)
| sK10 = sK12
| ~ rpoint(sK10)
| ~ rpoint(sK12) ),
inference(duplicate_literal_removal,[],[f2251]) ).
fof(f2253,plain,
! [X0] :
( ~ ron(sK11,X0)
| sK46(sK12,sK10) = X0
| ~ rcenter(sK12,X0)
| ~ rpoint(sK10)
| ~ rpoint(sK12) ),
inference(forward_subsumption_resolution,[],[f2252,f832]) ).
fof(f2254,plain,
! [X0] :
( ~ ron(sK11,X0)
| sK46(sK12,sK10) = X0
| ~ rcenter(sK12,X0)
| ~ rpoint(sK12) ),
inference(forward_subsumption_resolution,[],[f2253,f555]) ).
fof(f2255,plain,
! [X0] :
( ~ rcenter(sK12,X0)
| sK46(sK12,sK10) = X0
| ~ ron(sK11,X0) ),
inference(forward_subsumption_resolution,[],[f2254,f551]) ).
fof(f2256,plain,
! [X0] :
( sK46(sK12,X0) = sK46(sK12,sK10)
| ~ ron(sK11,sK46(sK12,X0))
| sK12 = X0
| ~ rpoint(X0)
| ~ rpoint(sK12) ),
inference(resolution,[],[f2255,f1498]) ).
fof(f2257,plain,
! [X0] :
( ~ ron(sK11,sK46(sK12,X0))
| sK46(sK12,X0) = sK46(sK12,sK10)
| sK12 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2256,f551]) ).
fof(f2258,plain,
( sK46(sK12,sK10) = sK46(sK12,sK11)
| sK11 = sK12
| ~ rpoint(sK11)
| sK11 = sK12
| ~ rpoint(sK11)
| ~ rpoint(sK12) ),
inference(resolution,[],[f2257,f1496]) ).
fof(f2259,plain,
( sK46(sK12,sK10) = sK46(sK12,sK11)
| sK11 = sK12
| ~ rpoint(sK11)
| ~ rpoint(sK12) ),
inference(duplicate_literal_removal,[],[f2258]) ).
fof(f2260,plain,
( sK46(sK12,sK10) = sK46(sK12,sK11)
| ~ rpoint(sK11)
| ~ rpoint(sK12) ),
inference(forward_subsumption_resolution,[],[f2259,f833]) ).
fof(f2261,plain,
( sK46(sK12,sK10) = sK46(sK12,sK11)
| ~ rpoint(sK12) ),
inference(forward_subsumption_resolution,[],[f2260,f553]) ).
fof(f2262,plain,
sK46(sK12,sK10) = sK46(sK12,sK11),
inference(forward_subsumption_resolution,[],[f2261,f551]) ).
fof(f2264,plain,
( rinside(sK12,sK46(sK12,sK10))
| sK11 = sK12
| ~ rpoint(sK11)
| ~ rpoint(sK12) ),
inference(superposition,[],[f2112,f2262]) ).
fof(f2265,plain,
( rcircle(sK46(sK12,sK10))
| sK11 = sK12
| ~ rpoint(sK11)
| ~ rpoint(sK12) ),
inference(superposition,[],[f1500,f2262]) ).
fof(f2266,plain,
( rcenter(sK12,sK46(sK12,sK10))
| sK11 = sK12
| ~ rpoint(sK11)
| ~ rpoint(sK12) ),
inference(superposition,[],[f1498,f2262]) ).
fof(f2267,plain,
( ron(sK11,sK46(sK12,sK10))
| sK11 = sK12
| ~ rpoint(sK11)
| ~ rpoint(sK12) ),
inference(superposition,[],[f1496,f2262]) ).
fof(f2268,plain,
( ron(sK11,sK46(sK12,sK10))
| ~ rpoint(sK11)
| ~ rpoint(sK12) ),
inference(forward_subsumption_resolution,[],[f2267,f833]) ).
fof(f2269,plain,
( rcenter(sK12,sK46(sK12,sK10))
| ~ rpoint(sK11)
| ~ rpoint(sK12) ),
inference(forward_subsumption_resolution,[],[f2266,f833]) ).
fof(f2270,plain,
( rcircle(sK46(sK12,sK10))
| ~ rpoint(sK11)
| ~ rpoint(sK12) ),
inference(forward_subsumption_resolution,[],[f2265,f833]) ).
fof(f2271,plain,
( rinside(sK12,sK46(sK12,sK10))
| ~ rpoint(sK11)
| ~ rpoint(sK12) ),
inference(forward_subsumption_resolution,[],[f2264,f833]) ).
fof(f2272,plain,
( ron(sK11,sK46(sK12,sK10))
| ~ rpoint(sK12) ),
inference(forward_subsumption_resolution,[],[f2268,f553]) ).
fof(f2273,plain,
( rcenter(sK12,sK46(sK12,sK10))
| ~ rpoint(sK12) ),
inference(forward_subsumption_resolution,[],[f2269,f553]) ).
fof(f2274,plain,
( rcircle(sK46(sK12,sK10))
| ~ rpoint(sK12) ),
inference(forward_subsumption_resolution,[],[f2270,f553]) ).
fof(f2275,plain,
( rinside(sK12,sK46(sK12,sK10))
| ~ rpoint(sK12) ),
inference(forward_subsumption_resolution,[],[f2271,f553]) ).
fof(f2276,plain,
ron(sK11,sK46(sK12,sK10)),
inference(forward_subsumption_resolution,[],[f2272,f551]) ).
fof(f2277,plain,
rcenter(sK12,sK46(sK12,sK10)),
inference(forward_subsumption_resolution,[],[f2273,f551]) ).
fof(f2278,plain,
rcircle(sK46(sK12,sK10)),
inference(forward_subsumption_resolution,[],[f2274,f551]) ).
fof(f2279,plain,
rinside(sK12,sK46(sK12,sK10)),
inference(forward_subsumption_resolution,[],[f2275,f551]) ).
fof(f2521,plain,
! [X0,X1] :
( vf(sK12,sK10) != vf(sK12,X0)
| ron(X0,X1)
| ~ ron(sK11,X1)
| ~ rpoint(sK11)
| ~ rcenter(sK12,X1)
| ~ rpoint(X0) ),
inference(superposition,[],[f1577,f830]) ).
fof(f2532,plain,
! [X0,X1] :
( vf(sK12,sK10) != vf(sK12,X0)
| ron(X0,X1)
| ~ ron(sK11,X1)
| ~ rcenter(sK12,X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2521,f553]) ).
fof(f2576,plain,
! [X0] :
( ron(sK10,X0)
| ~ ron(sK11,X0)
| ~ rcenter(sK12,X0)
| ~ rpoint(sK10) ),
inference(equality_resolution,[],[f2532]) ).
fof(f2577,plain,
! [X0] :
( ~ rcenter(sK12,X0)
| ~ ron(sK11,X0)
| ron(sK10,X0) ),
inference(forward_subsumption_resolution,[],[f2576,f555]) ).
fof(f2578,plain,
( ~ ron(sK11,sK46(sK12,sK10))
| ron(sK10,sK46(sK12,sK10)) ),
inference(resolution,[],[f2577,f2277]) ).
fof(f2581,plain,
ron(sK10,sK46(sK12,sK10)),
inference(forward_subsumption_resolution,[],[f2578,f2276]) ).
fof(f4065,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK10,X0,X1)
| rR(sK10,X2,X3)
| sK10 = X1
| sK10 = X3
| sK10 = X0
| sK10 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK10,X1) = vangle(X2,sK10,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK10) ),
inference(forward_subsumption_resolution,[],[f1758,f715]) ).
fof(f4213,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,vd1297)
| rR(sK10,X2,X3)
| sK10 = X1
| sK10 = X3
| sK10 = X0
| sK10 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| rR(sK10,X0,X1)
| ~ ron(X2,vd1297)
| vangle(X3,sK10,X1) = vangle(X2,sK10,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f4065,f555]) ).
fof(f4667,definition,
( spl52_106
<=> rR(sK10,sK11,sK12) ),
introduced(definition,[new_symbols(definition,[spl52_106])],[avatar_definition]) ).
fof(f4668,plain,
( rR(sK10,sK11,sK12)
| ~ spl52_106 ),
inference(avatar_component_clause,[],[f4667]) ).
fof(f4669,plain,
( ~ rR(sK10,sK11,sK12)
| spl52_106 ),
inference(avatar_component_clause,[],[f4667]) ).
fof(f4671,definition,
( spl52_107
<=> v0 = vangle(sK12,sK10,sK11) ),
introduced(definition,[new_symbols(definition,[spl52_107])],[avatar_definition]) ).
fof(f4672,plain,
( v0 = vangle(sK12,sK10,sK11)
| ~ spl52_107 ),
inference(avatar_component_clause,[],[f4671]) ).
fof(f4673,plain,
( v0 != vangle(sK12,sK10,sK11)
| spl52_107 ),
inference(avatar_component_clause,[],[f4671]) ).
fof(f4690,definition,
( spl52_110
<=> v0 = vangle(sK12,sK11,sK10) ),
introduced(definition,[new_symbols(definition,[spl52_110])],[avatar_definition]) ).
fof(f4691,plain,
( v0 = vangle(sK12,sK11,sK10)
| ~ spl52_110 ),
inference(avatar_component_clause,[],[f4690]) ).
fof(f4692,plain,
( v0 != vangle(sK12,sK11,sK10)
| spl52_110 ),
inference(avatar_component_clause,[],[f4690]) ).
fof(f5357,definition,
( spl52_188
<=> ! [X0] :
( ron(sK11,X0)
| ~ rline(X0)
| ~ ron(sK12,X0)
| ~ ron(sK10,X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_188])],[avatar_definition]) ).
fof(f5358,plain,
( ! [X0] :
( ~ ron(sK12,X0)
| ~ rline(X0)
| ron(sK11,X0)
| ~ ron(sK10,X0) )
| ~ spl52_188 ),
inference(avatar_component_clause,[],[f5357]) ).
fof(f5834,plain,
( ! [X0] :
( ~ rline(sK9(sK12,X0))
| ron(sK11,sK9(sK12,X0))
| ~ ron(sK10,sK9(sK12,X0))
| sK12 = X0
| ~ rpoint(X0)
| ~ rpoint(sK12) )
| ~ spl52_188 ),
inference(resolution,[],[f5358,f949]) ).
fof(f5839,plain,
( ! [X0] :
( ron(sK11,sK9(sK12,X0))
| ~ ron(sK10,sK9(sK12,X0))
| sK12 = X0
| ~ rpoint(X0)
| ~ rpoint(sK12) )
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f5834,f951]) ).
fof(f5842,plain,
( ! [X0] :
( ~ ron(sK10,sK9(sK12,X0))
| ron(sK11,sK9(sK12,X0))
| sK12 = X0
| ~ rpoint(X0) )
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f5839,f551]) ).
fof(f6230,plain,
( ron(sK11,sK9(sK12,sK10))
| sK10 = sK12
| ~ rpoint(sK10)
| sK10 = sK12
| ~ rpoint(sK10)
| ~ rpoint(sK12)
| ~ spl52_188 ),
inference(resolution,[],[f5842,f947]) ).
fof(f6231,plain,
( ron(sK11,sK9(sK12,sK10))
| sK10 = sK12
| ~ rpoint(sK10)
| ~ rpoint(sK12)
| ~ spl52_188 ),
inference(duplicate_literal_removal,[],[f6230]) ).
fof(f6232,plain,
( ron(sK11,sK9(sK12,sK10))
| ~ rpoint(sK10)
| ~ rpoint(sK12)
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6231,f832]) ).
fof(f6233,plain,
( ron(sK11,sK9(sK12,sK10))
| ~ rpoint(sK12)
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6232,f555]) ).
fof(f6234,plain,
( ron(sK11,sK9(sK12,sK10))
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6233,f551]) ).
fof(f6244,plain,
( ~ rpoint(sK12)
| rR(sK11,sK12,sK10)
| v0 = vangle(sK12,sK11,sK10)
| sK10 = sK12
| ~ rpoint(sK10)
| sK10 = sK11
| sK11 = sK12
| ~ rpoint(sK11)
| ~ spl52_188 ),
inference(resolution,[],[f6234,f1851]) ).
fof(f6269,plain,
( rR(sK11,sK12,sK10)
| v0 = vangle(sK12,sK11,sK10)
| sK10 = sK12
| ~ rpoint(sK10)
| sK10 = sK11
| sK11 = sK12
| ~ rpoint(sK11)
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6244,f551]) ).
fof(f6321,plain,
( rR(sK11,sK12,sK10)
| sK10 = sK12
| ~ rpoint(sK10)
| sK10 = sK11
| sK11 = sK12
| ~ rpoint(sK11)
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6269,f4692]) ).
fof(f6333,plain,
( rR(sK11,sK12,sK10)
| ~ rpoint(sK10)
| sK10 = sK11
| sK11 = sK12
| ~ rpoint(sK11)
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6321,f832]) ).
fof(f6345,plain,
( rR(sK11,sK12,sK10)
| sK10 = sK11
| sK11 = sK12
| ~ rpoint(sK11)
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6333,f555]) ).
fof(f6357,plain,
( rR(sK11,sK12,sK10)
| sK11 = sK12
| ~ rpoint(sK11)
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6345,f831]) ).
fof(f6365,plain,
( rR(sK11,sK12,sK10)
| ~ rpoint(sK11)
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6357,f833]) ).
fof(f6369,plain,
( rR(sK11,sK12,sK10)
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6365,f553]) ).
fof(f6384,plain,
( ! [X0] :
( ~ ron(sK10,X0)
| rinside(sK11,X0)
| ~ rinside(sK12,X0)
| ~ rcircle(X0)
| ~ rpoint(sK11)
| ~ rpoint(sK10)
| ~ rpoint(sK12) )
| spl52_110
| ~ spl52_188 ),
inference(resolution,[],[f6369,f1332]) ).
fof(f6387,plain,
( ! [X0] :
( ~ ron(sK10,X0)
| rinside(sK11,X0)
| ~ rinside(sK12,X0)
| ~ rcircle(X0)
| ~ rpoint(sK10)
| ~ rpoint(sK12) )
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6384,f553]) ).
fof(f6394,plain,
( ! [X0] :
( ~ ron(sK10,X0)
| rinside(sK11,X0)
| ~ rinside(sK12,X0)
| ~ rcircle(X0)
| ~ rpoint(sK12) )
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6387,f555]) ).
fof(f6401,plain,
( ! [X0] :
( ~ rinside(sK12,X0)
| rinside(sK11,X0)
| ~ ron(sK10,X0)
| ~ rcircle(X0) )
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f6394,f551]) ).
fof(f6715,definition,
( spl52_219
<=> rR(sK10,sK12,sK11) ),
introduced(definition,[new_symbols(definition,[spl52_219])],[avatar_definition]) ).
fof(f6716,plain,
( rR(sK10,sK12,sK11)
| ~ spl52_219 ),
inference(avatar_component_clause,[],[f6715]) ).
fof(f6906,plain,
( rR(sK10,sK12,sK11)
| ~ rpoint(sK12)
| ~ rpoint(sK10)
| ~ rpoint(sK11)
| ~ spl52_106 ),
inference(resolution,[],[f4668,f1175]) ).
fof(f6917,plain,
( rR(sK10,sK12,sK11)
| ~ rpoint(sK10)
| ~ rpoint(sK11)
| ~ spl52_106 ),
inference(forward_subsumption_resolution,[],[f6906,f551]) ).
fof(f6925,plain,
( rR(sK10,sK12,sK11)
| ~ rpoint(sK11)
| ~ spl52_106 ),
inference(forward_subsumption_resolution,[],[f6917,f555]) ).
fof(f6933,plain,
( rR(sK10,sK12,sK11)
| ~ spl52_106 ),
inference(forward_subsumption_resolution,[],[f6925,f553]) ).
fof(f6937,plain,
( spl52_219
| ~ spl52_106 ),
inference(avatar_split_clause,[],[f6933,f4667,f6715]) ).
fof(f7147,plain,
( ! [X2,X3,X0,X1] :
( rR(sK10,X0,sK12)
| sK10 = X1
| sK10 = sK12
| sK10 = X2
| sK10 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK10,X2,X1)
| ~ ron(X0,vd1297)
| vangle(sK12,sK10,X1) = vangle(X0,sK10,X2)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK12)
| ~ rpoint(X2)
| ~ rpoint(X0) )
| ~ spl52_2 ),
inference(resolution,[],[f4213,f1595]) ).
fof(f7148,plain,
( ! [X2,X3,X0,X1] :
( rR(sK10,X0,sK12)
| sK10 = X1
| sK10 = X2
| sK10 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK10,X2,X1)
| ~ ron(X0,vd1297)
| vangle(sK12,sK10,X1) = vangle(X0,sK10,X2)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK12)
| ~ rpoint(X2)
| ~ rpoint(X0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f7147,f832]) ).
fof(f7149,plain,
( ! [X2,X3,X0,X1] :
( ~ ron(X2,X3)
| sK10 = X1
| sK10 = X2
| sK10 = X0
| ~ ron(X1,X3)
| rR(sK10,X0,sK12)
| rR(sK10,X2,X1)
| ~ ron(X0,vd1297)
| vangle(sK12,sK10,X1) = vangle(X0,sK10,X2)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f7148,f551]) ).
fof(f7596,plain,
( ! [X0,X1] :
( sK10 = X0
| sK10 = sK11
| sK10 = X1
| ~ ron(X0,vd1295)
| rR(sK10,X1,sK12)
| rR(sK10,sK11,X0)
| ~ ron(X1,vd1297)
| vangle(sK12,sK10,X0) = vangle(X1,sK10,sK11)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK11)
| ~ rpoint(X1) )
| ~ spl52_2 ),
inference(resolution,[],[f7149,f851]) ).
fof(f7613,plain,
( ! [X0,X1] :
( sK10 = X0
| sK10 = X1
| ~ ron(X0,vd1295)
| rR(sK10,X1,sK12)
| rR(sK10,sK11,X0)
| ~ ron(X1,vd1297)
| vangle(sK12,sK10,X0) = vangle(X1,sK10,sK11)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK11)
| ~ rpoint(X1) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f7596,f831]) ).
fof(f7617,plain,
( ! [X0,X1] :
( sK10 = X0
| sK10 = X1
| ~ ron(X0,vd1295)
| rR(sK10,X1,sK12)
| rR(sK10,sK11,X0)
| ~ ron(X1,vd1297)
| vangle(sK12,sK10,X0) = vangle(X1,sK10,sK11)
| ~ rpoint(X0)
| ~ rpoint(sK11)
| ~ rpoint(X1) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f7613,f695]) ).
fof(f7621,plain,
( ! [X0,X1] :
( rR(sK10,sK11,X0)
| rR(sK10,X1,sK12)
| ~ ron(X0,vd1295)
| sK10 = X1
| sK10 = X0
| ~ ron(X1,vd1297)
| vangle(sK12,sK10,X0) = vangle(X1,sK10,sK11)
| ~ rpoint(X0)
| ~ rpoint(X1) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f7617,f553]) ).
fof(f8982,plain,
( ! [X0] :
( rR(sK10,X0,sK12)
| ~ ron(sK12,vd1295)
| sK10 = X0
| sK10 = sK12
| ~ ron(X0,vd1297)
| vangle(sK12,sK10,sK12) = vangle(X0,sK10,sK11)
| ~ rpoint(sK12)
| ~ rpoint(X0) )
| ~ spl52_2
| spl52_106 ),
inference(resolution,[],[f7621,f4669]) ).
fof(f9053,plain,
( ! [X0] :
( rR(sK10,X0,sK12)
| sK10 = X0
| sK10 = sK12
| ~ ron(X0,vd1297)
| vangle(sK12,sK10,sK12) = vangle(X0,sK10,sK11)
| ~ rpoint(sK12)
| ~ rpoint(X0) )
| ~ spl52_2
| ~ spl52_9
| spl52_106 ),
inference(forward_subsumption_resolution,[],[f8982,f1625]) ).
fof(f9077,plain,
( ! [X0] :
( rR(sK10,X0,sK12)
| sK10 = X0
| ~ ron(X0,vd1297)
| vangle(sK12,sK10,sK12) = vangle(X0,sK10,sK11)
| ~ rpoint(sK12)
| ~ rpoint(X0) )
| ~ spl52_2
| ~ spl52_9
| spl52_106 ),
inference(forward_subsumption_resolution,[],[f9053,f832]) ).
fof(f9082,plain,
( ! [X0] :
( rR(sK10,X0,sK12)
| sK10 = X0
| ~ ron(X0,vd1297)
| vangle(sK12,sK10,sK12) = vangle(X0,sK10,sK11)
| ~ rpoint(X0) )
| ~ spl52_2
| ~ spl52_9
| spl52_106 ),
inference(forward_subsumption_resolution,[],[f9077,f551]) ).
fof(f9087,plain,
( ! [X0] :
( rR(sK10,X0,sK12)
| v0 = vangle(X0,sK10,sK11)
| sK10 = X0
| ~ ron(X0,vd1297)
| ~ rpoint(X0) )
| ~ spl52_2
| ~ spl52_9
| spl52_106 ),
inference(forward_demodulation,[],[f9082,f2014]) ).
fof(f9101,plain,
( v0 = vangle(sK12,sK10,sK11)
| sK10 = sK12
| ~ ron(sK12,vd1297)
| ~ rpoint(sK12)
| ~ rpoint(sK12)
| ~ rpoint(sK10)
| ~ spl52_2
| ~ spl52_9
| spl52_106 ),
inference(resolution,[],[f9087,f1586]) ).
fof(f9104,plain,
( v0 = vangle(sK12,sK10,sK11)
| sK10 = sK12
| ~ ron(sK12,vd1297)
| ~ rpoint(sK12)
| ~ rpoint(sK10)
| ~ spl52_2
| ~ spl52_9
| spl52_106 ),
inference(duplicate_literal_removal,[],[f9101]) ).
fof(f9116,plain,
( sK10 = sK12
| ~ ron(sK12,vd1297)
| ~ rpoint(sK12)
| ~ rpoint(sK10)
| ~ spl52_2
| ~ spl52_9
| spl52_106
| spl52_107 ),
inference(forward_subsumption_resolution,[],[f9104,f4673]) ).
fof(f9127,plain,
( ~ ron(sK12,vd1297)
| ~ rpoint(sK12)
| ~ rpoint(sK10)
| ~ spl52_2
| ~ spl52_9
| spl52_106
| spl52_107 ),
inference(forward_subsumption_resolution,[],[f9116,f832]) ).
fof(f9138,plain,
( ~ rpoint(sK12)
| ~ rpoint(sK10)
| ~ spl52_2
| ~ spl52_9
| spl52_106
| spl52_107 ),
inference(forward_subsumption_resolution,[],[f9127,f1595]) ).
fof(f9140,plain,
( ~ rpoint(sK10)
| ~ spl52_2
| ~ spl52_9
| spl52_106
| spl52_107 ),
inference(forward_subsumption_resolution,[],[f9138,f551]) ).
fof(f9142,plain,
( $false
| ~ spl52_2
| ~ spl52_9
| spl52_106
| spl52_107 ),
inference(forward_subsumption_resolution,[],[f9140,f555]) ).
fof(f9143,plain,
( ~ spl52_2
| ~ spl52_9
| spl52_106
| spl52_107 ),
inference(avatar_contradiction_clause,[],[f9142]) ).
fof(f9152,plain,
( ! [X0] :
( v0 != v0
| ron(sK11,X0)
| ~ ron(sK12,X0)
| ~ ron(sK10,X0)
| sK10 = sK11
| sK10 = sK12
| ~ rline(X0)
| ~ rpoint(sK11)
| ~ rpoint(sK12)
| ~ rpoint(sK10) )
| ~ spl52_107 ),
inference(superposition,[],[f1567,f4672]) ).
fof(f9153,plain,
( ! [X0] :
( ron(sK11,X0)
| ~ ron(sK12,X0)
| ~ ron(sK10,X0)
| sK10 = sK11
| sK10 = sK12
| ~ rline(X0)
| ~ rpoint(sK11)
| ~ rpoint(sK12)
| ~ rpoint(sK10) )
| ~ spl52_107 ),
inference(trivial_inequality_removal,[],[f9152]) ).
fof(f9155,plain,
( ! [X0] :
( ron(sK11,X0)
| ~ ron(sK12,X0)
| ~ ron(sK10,X0)
| sK10 = sK12
| ~ rline(X0)
| ~ rpoint(sK11)
| ~ rpoint(sK12)
| ~ rpoint(sK10) )
| ~ spl52_107 ),
inference(forward_subsumption_resolution,[],[f9153,f831]) ).
fof(f9160,plain,
( ! [X0] :
( ron(sK11,X0)
| ~ ron(sK12,X0)
| ~ ron(sK10,X0)
| ~ rline(X0)
| ~ rpoint(sK11)
| ~ rpoint(sK12)
| ~ rpoint(sK10) )
| ~ spl52_107 ),
inference(forward_subsumption_resolution,[],[f9155,f832]) ).
fof(f9165,plain,
( ! [X0] :
( ron(sK11,X0)
| ~ ron(sK12,X0)
| ~ ron(sK10,X0)
| ~ rline(X0)
| ~ rpoint(sK12)
| ~ rpoint(sK10) )
| ~ spl52_107 ),
inference(forward_subsumption_resolution,[],[f9160,f553]) ).
fof(f9170,plain,
( ! [X0] :
( ron(sK11,X0)
| ~ ron(sK12,X0)
| ~ ron(sK10,X0)
| ~ rline(X0)
| ~ rpoint(sK10) )
| ~ spl52_107 ),
inference(forward_subsumption_resolution,[],[f9165,f551]) ).
fof(f9175,plain,
( ! [X0] :
( ron(sK11,X0)
| ~ ron(sK12,X0)
| ~ ron(sK10,X0)
| ~ rline(X0) )
| ~ spl52_107 ),
inference(forward_subsumption_resolution,[],[f9170,f555]) ).
fof(f9178,plain,
( spl52_188
| ~ spl52_107 ),
inference(avatar_split_clause,[],[f9175,f4671,f5357]) ).
fof(f9201,plain,
( ! [X0] :
( ~ ron(sK11,X0)
| rinside(sK10,X0)
| ~ rinside(sK12,X0)
| ~ rcircle(X0)
| ~ rpoint(sK10)
| ~ rpoint(sK11)
| ~ rpoint(sK12) )
| ~ spl52_219 ),
inference(resolution,[],[f6716,f1332]) ).
fof(f9204,plain,
( ! [X0] :
( ~ ron(sK11,X0)
| rinside(sK10,X0)
| ~ rinside(sK12,X0)
| ~ rcircle(X0)
| ~ rpoint(sK11)
| ~ rpoint(sK12) )
| ~ spl52_219 ),
inference(forward_subsumption_resolution,[],[f9201,f555]) ).
fof(f9213,plain,
( ! [X0] :
( ~ ron(sK11,X0)
| rinside(sK10,X0)
| ~ rinside(sK12,X0)
| ~ rcircle(X0)
| ~ rpoint(sK12) )
| ~ spl52_219 ),
inference(forward_subsumption_resolution,[],[f9204,f553]) ).
fof(f9222,plain,
( ! [X0] :
( ~ rinside(sK12,X0)
| rinside(sK10,X0)
| ~ ron(sK11,X0)
| ~ rcircle(X0) )
| ~ spl52_219 ),
inference(forward_subsumption_resolution,[],[f9213,f551]) ).
fof(f9558,plain,
( v0 != vangle(sK12,sK10,sK11)
| spl52_15
| ~ spl52_110 ),
inference(superposition,[],[f1659,f4691]) ).
fof(f10414,plain,
( rinside(sK10,sK46(sK12,sK10))
| ~ ron(sK11,sK46(sK12,sK10))
| ~ rcircle(sK46(sK12,sK10))
| ~ spl52_219 ),
inference(resolution,[],[f9222,f2279]) ).
fof(f10417,plain,
( rinside(sK10,sK46(sK12,sK10))
| ~ rcircle(sK46(sK12,sK10))
| ~ spl52_219 ),
inference(forward_subsumption_resolution,[],[f10414,f2276]) ).
fof(f10419,plain,
( rinside(sK10,sK46(sK12,sK10))
| ~ spl52_219 ),
inference(forward_subsumption_resolution,[],[f10417,f2278]) ).
fof(f10526,plain,
( ~ ron(sK10,sK46(sK12,sK10))
| ~ rcircle(sK46(sK12,sK10))
| ~ rpoint(sK10)
| ~ spl52_219 ),
inference(resolution,[],[f10419,f1433]) ).
fof(f10531,plain,
( ~ rcircle(sK46(sK12,sK10))
| ~ rpoint(sK10)
| ~ spl52_219 ),
inference(forward_subsumption_resolution,[],[f10526,f2581]) ).
fof(f10535,plain,
( ~ rpoint(sK10)
| ~ spl52_219 ),
inference(forward_subsumption_resolution,[],[f10531,f2278]) ).
fof(f10537,plain,
( $false
| ~ spl52_219 ),
inference(forward_subsumption_resolution,[],[f10535,f555]) ).
fof(f10538,plain,
~ spl52_219,
inference(avatar_contradiction_clause,[],[f10537]) ).
fof(f10543,plain,
( $false
| spl52_15
| ~ spl52_107
| ~ spl52_110 ),
inference(forward_subsumption_resolution,[],[f9558,f4672]) ).
fof(f10544,plain,
( spl52_15
| ~ spl52_107
| ~ spl52_110 ),
inference(avatar_contradiction_clause,[],[f10543]) ).
fof(f18471,plain,
( rinside(sK11,sK46(sK12,sK10))
| ~ ron(sK10,sK46(sK12,sK10))
| ~ rcircle(sK46(sK12,sK10))
| spl52_110
| ~ spl52_188 ),
inference(resolution,[],[f6401,f2279]) ).
fof(f18474,plain,
( rinside(sK11,sK46(sK12,sK10))
| ~ rcircle(sK46(sK12,sK10))
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f18471,f2581]) ).
fof(f18476,plain,
( rinside(sK11,sK46(sK12,sK10))
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f18474,f2278]) ).
fof(f18479,plain,
( ~ ron(sK11,sK46(sK12,sK10))
| ~ rcircle(sK46(sK12,sK10))
| ~ rpoint(sK11)
| spl52_110
| ~ spl52_188 ),
inference(resolution,[],[f18476,f1433]) ).
fof(f18484,plain,
( ~ rcircle(sK46(sK12,sK10))
| ~ rpoint(sK11)
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f18479,f2276]) ).
fof(f18488,plain,
( ~ rpoint(sK11)
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f18484,f2278]) ).
fof(f18490,plain,
( $false
| spl52_110
| ~ spl52_188 ),
inference(forward_subsumption_resolution,[],[f18488,f553]) ).
fof(f18491,plain,
( spl52_110
| ~ spl52_188 ),
inference(avatar_contradiction_clause,[],[f18490]) ).
cnf(s2,plain,
spl52_2,
inference(sat_conversion,[],[f1597]) ).
cnf(s12,plain,
spl52_9,
inference(sat_conversion,[],[f1628]) ).
cnf(s41,plain,
~ spl52_15,
inference(sat_conversion,[],[f1754]) ).
cnf(s235,plain,
( ~ spl52_106
| spl52_219 ),
inference(sat_conversion,[],[f6937]) ).
cnf(s249,plain,
( ~ spl52_2
| ~ spl52_9
| spl52_106
| spl52_107 ),
inference(sat_conversion,[],[f9143]) ).
cnf(s250,plain,
( ~ spl52_107
| spl52_188 ),
inference(sat_conversion,[],[f9178]) ).
cnf(s286,plain,
~ spl52_219,
inference(sat_conversion,[],[f10538]) ).
cnf(s289,plain,
( spl52_15
| ~ spl52_107
| ~ spl52_110 ),
inference(sat_conversion,[],[f10544]) ).
cnf(s449,plain,
( spl52_110
| ~ spl52_188 ),
inference(sat_conversion,[],[f18491]) ).
cnf(s468,plain,
~ spl52_106,
inference(rat,[],[s235,s286]) ).
cnf(s488,plain,
spl52_107,
inference(rat,[],[s249,s12,s468,s2]) ).
cnf(s489,plain,
~ spl52_110,
inference(rat,[],[s289,s41,s488]) ).
cnf(s490,plain,
spl52_188,
inference(rat,[],[s250,s488]) ).
cnf(s492,plain,
$false,
inference(rat,[],[s449,s490,s489]) ).
fof(f18492,plain,
$false,
inference(avatar_sat_refutation,[],[s492]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO330+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.35 % Computer : n011.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 27 08:07:00 UTC 2026
% 0.04/0.36 % CPUTime :
% 0.04/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.04/0.39 Running first-order theorem proving
% 0.04/0.39 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.59/2.81 % (2084400)Detected formulas, will run a generic FOF schedule.
% 13.59/2.81 % (2084409)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1137288924:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.59/2.81 % (2084409)Instruction limit reached!
% 13.59/2.81 % (2084409)------------------------------
% 13.59/2.81 % (2084409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.59/2.81 % (2084409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.59/2.81 % (2084409)CaDiCaL version: 2.1.3
% 13.59/2.81 % (2084409)Termination reason: Instruction limit
% 13.59/2.81 % (2084409)Termination phase: Saturation
% 13.59/2.81 % (2084409)Time elapsed: 0.033 s
% 13.59/2.81 % (2084409)Peak memory usage: 88 MB
% 13.59/2.81 % (2084409)Instructions burned: 121 (million)
% 13.59/2.81 % (2084406)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=40971137:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.59/2.81 % (2084407)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=2105358945:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.59/2.81 % (2084410)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=194624500:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.59/2.81 % (2084405)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=1723290023:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.59/2.81 % (2084408)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3346105598:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.59/2.81 % (2084411)dis-21_1_sil=8000:lcm=predicate:random_seed=3259228588: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.59/2.81 % (2084408)Instruction limit reached!
% 13.59/2.81 % (2084408)------------------------------
% 13.59/2.81 % (2084408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.59/2.81 % (2084408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.59/2.81 % (2084408)CaDiCaL version: 2.1.3
% 13.59/2.81 % (2084408)Termination reason: Instruction limit
% 13.59/2.81 % (2084408)Termination phase: Saturation
% 13.59/2.81 % (2084408)Time elapsed: 0.058 s
% 13.59/2.81 % (2084408)Peak memory usage: 89 MB
% 13.59/2.81 % (2084408)Instructions burned: 111 (million)
% 13.59/2.81 % (2084411)Instruction limit reached!
% 13.59/2.81 % (2084411)------------------------------
% 13.59/2.81 % (2084411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.59/2.81 % (2084411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.59/2.81 % (2084411)CaDiCaL version: 2.1.3
% 13.59/2.81 % (2084411)Termination reason: Instruction limit
% 13.59/2.81 % (2084411)Termination phase: Saturation
% 13.59/2.81 % (2084411)Time elapsed: 0.068 s
% 13.59/2.81 % (2084411)Peak memory usage: 90 MB
% 13.59/2.81 % (2084411)Instructions burned: 129 (million)
% 13.59/2.81 % (2084410)Instruction limit reached!
% 13.59/2.81 % (2084410)------------------------------
% 13.59/2.81 % (2084410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.59/2.81 % (2084410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.59/2.81 % (2084410)CaDiCaL version: 2.1.3
% 13.59/2.81 % (2084410)Termination reason: Instruction limit
% 13.59/2.81 % (2084410)Termination phase: Saturation
% 13.59/2.81 % (2084410)Time elapsed: 0.086 s
% 13.59/2.81 % (2084410)Peak memory usage: 90 MB
% 13.59/2.81 % (2084410)Instructions burned: 141 (million)
% 13.59/2.81 % (2084413)lrs+10_1_sil=8000:sp=occurrence:random_seed=1882079405:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 13.59/2.81 % (2084413)Instruction limit reached!
% 13.59/2.81 % (2084413)------------------------------
% 13.59/2.81 % (2084413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.59/2.81 % (2084413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.59/2.81 % (2084413)CaDiCaL version: 2.1.3
% 13.59/2.81 % (2084413)Termination reason: Instruction limit
% 13.59/2.81 % (2084413)Termination phase: Saturation
% 13.59/2.81 % (2084413)Time elapsed: 0.074 s
% 13.59/2.81 % (2084413)Peak memory usage: 91 MB
% 13.59/2.81 % (2084413)Instructions burned: 288 (million)
% 17.29/3.38 % (2084421)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3432403888:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 17.29/3.38 % (2084420)lrs+10_1_sil=32000:urr=on:br=off:random_seed=185359838:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 17.29/3.38 % (2084422)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=1036528590:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 17.29/3.38 % (2084420)Instruction limit reached!
% 17.29/3.38 % (2084420)------------------------------
% 17.29/3.38 % (2084420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.29/3.38 % (2084420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.29/3.38 % (2084420)CaDiCaL version: 2.1.3
% 17.29/3.38 % (2084420)Termination reason: Instruction limit
% 17.29/3.38 % (2084420)Termination phase: Saturation
% 17.29/3.38 % (2084420)Time elapsed: 0.079 s
% 17.29/3.38 % (2084420)Peak memory usage: 89 MB
% 17.29/3.38 % (2084420)Instructions burned: 158 (million)
% 17.29/3.38 % (2084424)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3944875888:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 17.29/3.38 % (2084422)Instruction limit reached!
% 17.29/3.38 % (2084422)------------------------------
% 17.29/3.38 % (2084422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.29/3.38 % (2084422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.29/3.38 % (2084422)CaDiCaL version: 2.1.3
% 17.29/3.38 % (2084422)Termination reason: Instruction limit
% 17.29/3.38 % (2084422)Termination phase: Saturation
% 17.29/3.38 % (2084422)Time elapsed: 0.120 s
% 17.29/3.38 % (2084422)Peak memory usage: 90 MB
% 17.29/3.38 % (2084422)Instructions burned: 249 (million)
% 17.29/3.38 % (2084424)Instruction limit reached!
% 17.29/3.38 % (2084424)------------------------------
% 17.29/3.38 % (2084424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.29/3.38 % (2084424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.29/3.38 % (2084424)CaDiCaL version: 2.1.3
% 17.29/3.38 % (2084424)Termination reason: Instruction limit
% 17.29/3.38 % (2084424)Termination phase: Saturation
% 17.29/3.38 % (2084424)Time elapsed: 0.071 s
% 17.29/3.38 % (2084424)Peak memory usage: 89 MB
% 17.29/3.38 % (2084424)Instructions burned: 298 (million)
% 17.29/3.38 % (2084421)Instruction limit reached!
% 17.29/3.38 % (2084421)------------------------------
% 17.29/3.38 % (2084421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.29/3.38 % (2084421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.29/3.38 % (2084421)CaDiCaL version: 2.1.3
% 17.29/3.38 % (2084421)Termination reason: Instruction limit
% 17.29/3.38 % (2084421)Termination phase: Saturation
% 17.29/3.38 % (2084421)Time elapsed: 0.183 s
% 17.29/3.38 % (2084421)Peak memory usage: 91 MB
% 17.29/3.38 % (2084421)Instructions burned: 325 (million)
% 17.29/3.38 % (2084429)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1013508850:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 17.29/3.38 % (2084431)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=604251609:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 17.29/3.38 % (2084431)Refutation not found, incomplete strategy
% 17.29/3.38 % (2084431)------------------------------
% 17.29/3.38 % (2084431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.29/3.38 % (2084431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.29/3.38 % (2084431)CaDiCaL version: 2.1.3
% 17.29/3.38 % (2084431)Termination reason: Refutation not found, incomplete strategy
% 17.29/3.38 % (2084431)Time elapsed: 0.017 s
% 17.29/3.38 % (2084431)Peak memory usage: 89 MB
% 17.29/3.38 % (2084431)Instructions burned: 63 (million)
% 17.29/3.38 % (2084430)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=288302252:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 17.29/3.38 % (2084432)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3377441696:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 17.29/3.38 % (2084430)Instruction limit reached!
% 17.29/3.38 % (2084430)------------------------------
% 17.29/3.38 % (2084430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.29/3.38 % (2084430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.46 % (2084430)CaDiCaL version: 2.1.3
% 25.37/4.46 % (2084430)Termination reason: Instruction limit
% 25.37/4.46 % (2084430)Termination phase: Saturation
% 25.37/4.46 % (2084430)Time elapsed: 0.060 s
% 25.37/4.46 % (2084430)Peak memory usage: 90 MB
% 25.37/4.46 % (2084430)Instructions burned: 115 (million)
% 25.37/4.46 % (2084432)Instruction limit reached!
% 25.37/4.46 % (2084432)------------------------------
% 25.37/4.46 % (2084432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.46 % (2084432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.46 % (2084432)CaDiCaL version: 2.1.3
% 25.37/4.46 % (2084432)Termination reason: Instruction limit
% 25.37/4.46 % (2084432)Termination phase: Saturation
% 25.37/4.46 % (2084432)Time elapsed: 0.053 s
% 25.37/4.46 % (2084432)Peak memory usage: 89 MB
% 25.37/4.46 % (2084432)Instructions burned: 116 (million)
% 25.37/4.46 % (2084431)------------------------------
% 25.37/4.46 % (2084431)------------------------------
% 25.37/4.46 % (2084437)lrs+10_1_sil=8000:sp=occurrence:random_seed=425303617:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 25.37/4.46 % (2084439)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=863335126:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 25.37/4.46 % (2084438)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2100262756:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 25.37/4.46 % (2084438)Refutation not found, incomplete strategy
% 25.37/4.46 % (2084438)------------------------------
% 25.37/4.46 % (2084438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.46 % (2084438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.46 % (2084438)CaDiCaL version: 2.1.3
% 25.37/4.46 % (2084438)Termination reason: Refutation not found, incomplete strategy
% 25.37/4.46 % (2084438)Time elapsed: 0.018 s
% 25.37/4.46 % (2084438)Peak memory usage: 89 MB
% 25.37/4.46 % (2084438)Instructions burned: 35 (million)
% 25.37/4.46 % (2084438)------------------------------
% 25.37/4.46 % (2084438)------------------------------
% 25.37/4.46 % (2084443)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=108620055:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 25.37/4.46 % (2084437)Instruction limit reached!
% 25.37/4.46 % (2084437)------------------------------
% 25.37/4.46 % (2084437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.46 % (2084437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.46 % (2084437)CaDiCaL version: 2.1.3
% 25.37/4.46 % (2084437)Termination reason: Instruction limit
% 25.37/4.46 % (2084437)Termination phase: Saturation
% 25.37/4.46 % (2084437)Time elapsed: 0.456 s
% 25.37/4.46 % (2084437)Peak memory usage: 97 MB
% 25.37/4.46 % (2084437)Instructions burned: 909 (million)
% 25.37/4.46 % (2084443)Instruction limit reached!
% 25.37/4.46 % (2084443)------------------------------
% 25.37/4.46 % (2084443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.46 % (2084443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.46 % (2084443)CaDiCaL version: 2.1.3
% 25.37/4.46 % (2084443)Termination reason: Instruction limit
% 25.37/4.46 % (2084443)Termination phase: Saturation
% 25.37/4.46 % (2084443)Time elapsed: 0.067 s
% 25.37/4.46 % (2084443)Peak memory usage: 93 MB
% 25.37/4.46 % (2084443)Instructions burned: 135 (million)
% 25.37/4.46 % (2084445)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1553328326:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 25.37/4.46 % (2084446)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2907900108:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 25.37/4.46 % (2084445)Instruction limit reached!
% 25.37/4.46 % (2084445)------------------------------
% 25.37/4.46 % (2084445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.46 % (2084445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.46 % (2084445)CaDiCaL version: 2.1.3
% 25.37/4.46 % (2084445)Termination reason: Instruction limit
% 25.37/4.46 % (2084445)Termination phase: Saturation
% 25.37/4.46 % (2084445)Time elapsed: 0.293 s
% 25.37/4.46 % (2084445)Peak memory usage: 93 MB
% 25.37/4.46 % (2084445)Instructions burned: 592 (million)
% 25.37/4.46 % (2084449)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=764203211:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 30.74/5.19 % (2084449)Refutation not found, incomplete strategy
% 30.74/5.19 % (2084449)------------------------------
% 30.74/5.19 % (2084449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.19 % (2084449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.19 % (2084449)CaDiCaL version: 2.1.3
% 30.74/5.19 % (2084449)Termination reason: Refutation not found, incomplete strategy
% 30.74/5.19 % (2084449)Time elapsed: 0.016 s
% 30.74/5.19 % (2084449)Peak memory usage: 89 MB
% 30.74/5.19 % (2084449)Instructions burned: 29 (million)
% 30.74/5.19 % (2084429)Instruction limit reached!
% 30.74/5.19 % (2084429)------------------------------
% 30.74/5.19 % (2084429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.19 % (2084429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.19 % (2084429)CaDiCaL version: 2.1.3
% 30.74/5.19 % (2084429)Termination reason: Instruction limit
% 30.74/5.19 % (2084429)Termination phase: Saturation
% 30.74/5.19 % (2084429)Time elapsed: 1.502 s
% 30.74/5.19 % (2084429)Peak memory usage: 142 MB
% 30.74/5.19 % (2084429)Instructions burned: 2351 (million)
% 30.74/5.19 % (2084449)------------------------------
% 30.74/5.19 % (2084449)------------------------------
% 30.74/5.19 % (2084439)Instruction limit reached!
% 30.74/5.19 % (2084439)------------------------------
% 30.74/5.19 % (2084439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.19 % (2084439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.19 % (2084439)CaDiCaL version: 2.1.3
% 30.74/5.19 % (2084439)Termination reason: Instruction limit
% 30.74/5.19 % (2084439)Termination phase: Saturation
% 30.74/5.19 % (2084439)Time elapsed: 1.314 s
% 30.74/5.19 % (2084439)Peak memory usage: 139 MB
% 30.74/5.19 % (2084439)Instructions burned: 5204 (million)
% 30.74/5.19 % (2084451)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4071675995:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 30.74/5.19 % (2084453)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3803886019:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 30.74/5.19 % (2084452)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3247202726:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 30.74/5.19 % (2084453)Refutation not found, incomplete strategy
% 30.74/5.19 % (2084453)------------------------------
% 30.74/5.19 % (2084453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.19 % (2084453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.19 % (2084453)CaDiCaL version: 2.1.3
% 30.74/5.19 % (2084453)Termination reason: Refutation not found, incomplete strategy
% 30.74/5.19 % (2084453)Time elapsed: 0.004 s
% 30.74/5.19 % (2084453)Peak memory usage: 88 MB
% 30.74/5.19 % (2084453)Instructions burned: 11 (million)
% 30.74/5.19 % (2084452)Refutation not found, incomplete strategy
% 30.74/5.19 % (2084452)------------------------------
% 30.74/5.19 % (2084452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.19 % (2084452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.19 % (2084452)CaDiCaL version: 2.1.3
% 30.74/5.19 % (2084452)Termination reason: Refutation not found, incomplete strategy
% 30.74/5.19 % (2084452)Time elapsed: 0.004 s
% 30.74/5.19 % (2084452)Peak memory usage: 88 MB
% 30.74/5.19 % (2084452)Instructions burned: 5 (million)
% 30.74/5.19 % (2084451)Instruction limit reached!
% 30.74/5.19 % (2084451)------------------------------
% 30.74/5.19 % (2084451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.19 % (2084451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.19 % (2084451)CaDiCaL version: 2.1.3
% 30.74/5.19 % (2084451)Termination reason: Instruction limit
% 30.74/5.19 % (2084451)Termination phase: Saturation
% 30.74/5.19 % (2084451)Time elapsed: 0.079 s
% 30.74/5.19 % (2084451)Peak memory usage: 91 MB
% 30.74/5.19 % (2084451)Instructions burned: 135 (million)
% 30.74/5.19 % (2084453)------------------------------
% 30.74/5.19 % (2084453)------------------------------
% 30.74/5.19 % (2084457)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=1353259318:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 30.74/5.19 % (2084452)------------------------------
% 30.74/5.19 % (2084452)------------------------------
% 30.74/5.19 % (2084458)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=3998639806:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 30.74/5.19 % (2084458)Instruction limit reached!
% 30.74/5.19 % (2084458)------------------------------
% 30.74/5.19 % (2084458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.19 % (2084458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.19 % (2084458)CaDiCaL version: 2.1.3
% 30.74/5.19 % (2084458)Termination reason: Instruction limit
% 30.74/5.19 % (2084458)Termination phase: Saturation
% 30.74/5.19 % (2084458)Time elapsed: 0.041 s
% 30.74/5.19 % (2084458)Peak memory usage: 92 MB
% 30.74/5.19 % (2084458)Instructions burned: 151 (million)
% 30.74/5.19 % (2084460)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2950756316:i=14155:bd=all_2973 on theBenchmark for (2973ds/14155Mi)
% 30.74/5.19 % (2084462)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2334735987:i=667:av=off:fsr=off_2973 on theBenchmark for (2973ds/667Mi)
% 30.74/5.19 % (2084462)Refutation not found, incomplete strategy
% 30.74/5.19 % (2084462)------------------------------
% 30.74/5.19 % (2084462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.19 % (2084462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.19 % (2084462)CaDiCaL version: 2.1.3
% 30.74/5.19 % (2084462)Termination reason: Refutation not found, incomplete strategy
% 30.74/5.19 % (2084462)Time elapsed: 0.013 s
% 30.74/5.19 % (2084462)Peak memory usage: 89 MB
% 30.74/5.19 % (2084462)Instructions burned: 47 (million)
% 30.74/5.19 % (2084462)------------------------------
% 30.74/5.19 % (2084462)------------------------------
% 30.74/5.19 % (2084465)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=2797955448:s2a=on:i=185:s2at=1.8:fdi=4_2970 on theBenchmark for (2970ds/185Mi)
% 30.74/5.19 % (2084465)Instruction limit reached!
% 30.74/5.19 % (2084465)------------------------------
% 30.74/5.19 % (2084465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.19 % (2084465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.19 % (2084465)CaDiCaL version: 2.1.3
% 30.74/5.19 % (2084465)Termination reason: Instruction limit
% 30.74/5.19 % (2084465)Termination phase: Saturation
% 30.74/5.19 % (2084465)Time elapsed: 0.053 s
% 30.74/5.19 % (2084465)Peak memory usage: 93 MB
% 30.74/5.19 % (2084465)Instructions burned: 188 (million)
% 30.74/5.19 % (2084467)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3551954454:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2968 on theBenchmark for (2968ds/193Mi)
% 30.74/5.19 % (2084467)Instruction limit reached!
% 30.74/5.19 % (2084467)------------------------------
% 30.74/5.19 % (2084467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.19 % (2084467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.19 % (2084467)CaDiCaL version: 2.1.3
% 30.74/5.19 % (2084467)Termination reason: Instruction limit
% 30.74/5.19 % (2084467)Termination phase: Saturation
% 30.74/5.19 % (2084467)Time elapsed: 0.056 s
% 30.74/5.19 % (2084467)Peak memory usage: 90 MB
% 30.74/5.19 % (2084467)Instructions burned: 194 (million)
% 30.74/5.19 % (2084469)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2793720148:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2966 on theBenchmark for (2966ds/4850Mi)
% 30.74/5.19 % (2084469)Refutation not found, incomplete strategy
% 30.74/5.19 % (2084469)------------------------------
% 30.74/5.19 % (2084469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.19 % (2084469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.19 % (2084469)CaDiCaL version: 2.1.3
% 30.74/5.19 % (2084469)Termination reason: Refutation not found, incomplete strategy
% 30.74/5.19 % (2084469)Time elapsed: 0.009 s
% 30.74/5.19 % (2084469)Peak memory usage: 89 MB
% 30.74/5.19 % (2084469)Instructions burned: 34 (million)
% 30.74/5.19 % (2084469)------------------------------
% 30.74/5.19 % (2084469)------------------------------
% 30.74/5.19 % (2084471)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1555747164:i=12111:sd=1:ss=included_2963 on theBenchmark for (2963ds/12111Mi)
% 30.74/5.19 % (2084446)First to succeed.
% 30.74/5.19 % (2084446)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2084400"
% 30.74/5.19 % (2084446)Refutation found. Thanks to Tanya!
% 30.74/5.19 % SZS status Theorem for theBenchmark
% 30.74/5.19 % SZS output start Proof for theBenchmark
% See solution above
% 31.32/5.39 % (2084446)------------------------------
% 31.32/5.39 % (2084446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.32/5.39 % (2084446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.32/5.39 % (2084446)CaDiCaL version: 2.1.3
% 31.32/5.39 % (2084446)Termination reason: Refutation
% 31.32/5.39 % (2084446)Time elapsed: 2.499 s
% 31.32/5.39 % (2084446)Peak memory usage: 148 MB
% 31.32/5.39 % (2084446)Instructions burned: 4043 (million)
% 31.32/5.39 % (2084446)------------------------------
% 31.32/5.39 % (2084446)------------------------------
% 31.32/5.39 % (2084400)Success in time 4.36 s
% 31.32/5.39 % Vampire exiting
%------------------------------------------------------------------------------