%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO309+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:52:24 AM UTC 2026
% Result : Theorem 19.70s 4.14s
% Output : Refutation 23.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 48
% Syntax : Number of formulae : 541 ( 97 unt; 15 def)
% Number of atoms : 3325 (1064 equ)
% Maximal formula atoms : 26 ( 6 avg)
% Number of connectives : 4872 (2088 ~;2580 |; 171 &)
% ( 19 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 14 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 17 con; 0-3 aty)
% Number of variables : 1178 ( 0 sgn1129 !; 49 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vf(vd1299,vd1289) = vf(vd1306,vd1288),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(359), 1318, 0)') ).
fof(f2,negated_conjecture,
vf(vd1299,vd1289) != vf(vd1306,vd1288),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f5,axiom,
~ rR(vd1287,vd1289,vd1306),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','neg(neg(conjunct2(356)))') ).
fof(f8,axiom,
rpoint(vd1306),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(352, 0)') ).
fof(f9,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(f10,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(f11,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(f12,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(f13,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(f15,axiom,
vd1299 = vd1300,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(348, 4)') ).
fof(f16,axiom,
rpoint(vd1300),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(348, 1)') ).
fof(f21,axiom,
vd1306 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(353)), 1309, 0)') ).
fof(f22,axiom,
vf(vd1287,vd1299) = vf(vd1287,vd1306),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(352), 1308, 0)') ).
fof(f23,axiom,
vd1289 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(355)), 1313, 0)') ).
fof(f28,axiom,
vd1288 != vd1287,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(355), 1312, 0)') ).
fof(f33,axiom,
rline(vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(347, 0)') ).
fof(f36,axiom,
rline(vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(346, 0)') ).
fof(f42,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(f43,axiom,
ron(vd1289,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(354))))), 0)') ).
fof(f44,axiom,
ron(vd1288,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(354))))), 0)') ).
fof(f45,axiom,
ron(vd1306,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(conjunct2(conjunct2(354)))), 0)') ).
fof(f46,axiom,
ron(vd1287,vd1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(conjunct2(354))), 0)') ).
fof(f48,axiom,
ron(vd1287,vd1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(conjunct1(354), 0)') ).
fof(f51,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(f53,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(f58,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(f60,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(f61,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(f70,axiom,
! [X0,X1] :
( ( ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> vf(X0,X1) = vf(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(166), 0), imp(cond(axiom(166), 0)))') ).
fof(f74,axiom,
v0 = vd684,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(axiom(137), 2)') ).
fof(f78,axiom,
! [X0,X1,X2] :
( ( rR(X1,X0,X2)
& ? [X3] :
( X2 = X3
& rpoint(X3) )
& ? [X4] :
( X1 = X4
& rpoint(X4) )
& ? [X5] :
( X0 = X5
& rpoint(X5) ) )
=> vplus(vf(X0,X1),vf(X1,X2)) = vf(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(180), 0), imp(cond(axiom(180), 0)))') ).
fof(f80,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(f81,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(f95,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(f150,plain,
vf(vd1299,vd1289) != vf(vd1306,vd1288),
inference(flattening,[],[f2]) ).
fof(f155,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,[],[f11]) ).
fof(f156,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,[],[f155]) ).
fof(f157,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,[],[f12]) ).
fof(f158,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,[],[f157]) ).
fof(f159,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,[],[f13]) ).
fof(f160,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,[],[f159]) ).
fof(f177,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,[],[f42]) ).
fof(f178,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,[],[f177]) ).
fof(f183,plain,
! [X0,X1] :
( ? [X4] :
( vf(X0,X1) = X4
& rreal(X4) )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f51]) ).
fof(f184,plain,
! [X0,X1] :
( ? [X4] :
( vf(X0,X1) = X4
& rreal(X4) )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f183]) ).
fof(f187,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,[],[f53]) ).
fof(f188,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,[],[f187]) ).
fof(f197,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,[],[f58]) ).
fof(f198,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,[],[f197]) ).
fof(f201,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,[],[f60]) ).
fof(f202,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,[],[f201]) ).
fof(f203,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,[],[f61]) ).
fof(f204,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,[],[f203]) ).
fof(f221,plain,
! [X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f70]) ).
fof(f222,plain,
! [X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f221]) ).
fof(f233,plain,
! [X0,X1,X2] :
( vplus(vf(X0,X1),vf(X1,X2)) = vf(X0,X2)
| ~ rR(X1,X0,X2)
| ! [X3] :
( X2 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(ennf_transformation,[],[f78]) ).
fof(f234,plain,
! [X0,X1,X2] :
( vplus(vf(X0,X1),vf(X1,X2)) = vf(X0,X2)
| ~ rR(X1,X0,X2)
| ! [X3] :
( X2 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(flattening,[],[f233]) ).
fof(f237,plain,
! [X0,X1] :
( rinside(X0,X1)
| ~ rcenter(X0,X1) ),
inference(ennf_transformation,[],[f80]) ).
fof(f238,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,[],[f81]) ).
fof(f239,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,[],[f238]) ).
fof(f265,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,[],[f95]) ).
fof(f266,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,[],[f265]) ).
fof(f367,plain,
( vf(vd1287,vd1288) = vf(vd1287,vd1289)
& vd1288 != vd1289
& vd1287 != vd1289
& vd1287 != vd1288
& vd1289 = sK1
& rpoint(sK1)
& vd1288 = sK2
& rpoint(sK2)
& vd1287 = sK3
& rpoint(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3)],[f10]) ).
fof(f374,plain,
! [X0,X1] :
( ? [X2] :
( vf(X0,X1) = X2
& rreal(X2) )
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(rectify,[],[f184]) ).
fof(f375,plain,
! [X0,X1] :
( ( vf(X0,X1) = sK7(X0,X1)
& rreal(sK7(X0,X1)) )
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f374]) ).
fof(f376,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,[],[f188]) ).
fof(f377,plain,
! [X0,X1] :
( ( ron(X1,sK8(X0,X1))
& ron(X0,sK8(X0,X1))
& rline(sK8(X0,X1)) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X2,sK8(X0,X1))],[f376]) ).
fof(f380,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,[],[f198]) ).
fof(f381,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
| vangle(X2,X0,X4) != v0 )
& ( vangle(X2,X0,X4) = v0
| rR(X0,X2,X4)
| ~ ron(X4,X6) ) )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(flattening,[],[f380]) ).
fof(f383,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,[],[f202]) ).
fof(f390,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,[],[f239]) ).
fof(f391,plain,
! [X0,X1] :
( ( ron(X1,sK13(X0,X1))
& rcenter(X0,sK13(X0,X1))
& rcircle(sK13(X0,X1)) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X2,sK13(X0,X1))],[f390]) ).
fof(f443,plain,
vf(vd1299,vd1289) != vf(vd1306,vd1288),
inference(cnf_transformation,[],[f150]) ).
fof(f446,plain,
~ rR(vd1287,vd1289,vd1306),
inference(cnf_transformation,[],[f5]) ).
fof(f449,plain,
rpoint(vd1306),
inference(cnf_transformation,[],[f8]) ).
fof(f450,plain,
rR(vd1288,vd1287,vd1299),
inference(cnf_transformation,[],[f9]) ).
fof(f454,plain,
rpoint(sK3),
inference(cnf_transformation,[],[f367]) ).
fof(f455,plain,
vd1287 = sK3,
inference(cnf_transformation,[],[f367]) ).
fof(f456,plain,
rpoint(sK2),
inference(cnf_transformation,[],[f367]) ).
fof(f457,plain,
vd1288 = sK2,
inference(cnf_transformation,[],[f367]) ).
fof(f458,plain,
rpoint(sK1),
inference(cnf_transformation,[],[f367]) ).
fof(f459,plain,
vd1289 = sK1,
inference(cnf_transformation,[],[f367]) ).
fof(f462,plain,
vd1289 != vd1288,
inference(cnf_transformation,[],[f367]) ).
fof(f463,plain,
vf(vd1287,vd1288) = vf(vd1287,vd1289),
inference(cnf_transformation,[],[f367]) ).
fof(f464,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,[],[f156]) ).
fof(f465,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,[],[f158]) ).
fof(f466,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,[],[f160]) ).
fof(f467,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,[],[f160]) ).
fof(f468,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,[],[f160]) ).
fof(f469,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,[],[f160]) ).
fof(f471,plain,
vd1299 = vd1300,
inference(cnf_transformation,[],[f15]) ).
fof(f472,plain,
rpoint(vd1300),
inference(cnf_transformation,[],[f16]) ).
fof(f486,plain,
vd1306 != vd1287,
inference(cnf_transformation,[],[f21]) ).
fof(f487,plain,
vf(vd1287,vd1299) = vf(vd1287,vd1306),
inference(cnf_transformation,[],[f22]) ).
fof(f488,plain,
vd1289 != vd1287,
inference(cnf_transformation,[],[f23]) ).
fof(f493,plain,
vd1288 != vd1287,
inference(cnf_transformation,[],[f28]) ).
fof(f498,plain,
rline(vd1297),
inference(cnf_transformation,[],[f33]) ).
fof(f501,plain,
rline(vd1295),
inference(cnf_transformation,[],[f36]) ).
fof(f508,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,[],[f178]) ).
fof(f509,plain,
ron(vd1289,vd1297),
inference(cnf_transformation,[],[f43]) ).
fof(f510,plain,
ron(vd1288,vd1295),
inference(cnf_transformation,[],[f44]) ).
fof(f511,plain,
ron(vd1306,vd1297),
inference(cnf_transformation,[],[f45]) ).
fof(f512,plain,
ron(vd1287,vd1297),
inference(cnf_transformation,[],[f46]) ).
fof(f514,plain,
ron(vd1287,vd1295),
inference(cnf_transformation,[],[f48]) ).
fof(f518,plain,
! [X3,X0,X1,X4] :
( vf(X0,X1) = sK7(X0,X1)
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f375]) ).
fof(f520,plain,
! [X3,X0,X1,X4] :
( rline(sK8(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f377]) ).
fof(f521,plain,
! [X3,X0,X1,X4] :
( ron(X0,sK8(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f377]) ).
fof(f522,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK8(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f377]) ).
fof(f529,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,[],[f381]) ).
fof(f530,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,[],[f381]) ).
fof(f531,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,[],[f381]) ).
fof(f534,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,[],[f383]) ).
fof(f536,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,[],[f204]) ).
fof(f546,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f222]) ).
fof(f550,plain,
v0 = vd684,
inference(cnf_transformation,[],[f74]) ).
fof(f572,plain,
! [X2,X3,X0,X1,X4,X5] :
( vf(X0,X2) = vplus(vf(X0,X1),vf(X1,X2))
| ~ rR(X1,X0,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(cnf_transformation,[],[f234]) ).
fof(f574,plain,
! [X0,X1] :
( ~ rcenter(X0,X1)
| rinside(X0,X1) ),
inference(cnf_transformation,[],[f237]) ).
fof(f575,plain,
! [X3,X0,X1,X4] :
( rcircle(sK13(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f391]) ).
fof(f576,plain,
! [X3,X0,X1,X4] :
( rcenter(X0,sK13(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f391]) ).
fof(f577,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK13(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f391]) ).
fof(f605,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,[],[f266]) ).
fof(f735,plain,
vf(vd1300,sK1) != vf(vd1306,sK2),
inference(definition_unfolding,[],[f443,f471,f459,f457]) ).
fof(f738,plain,
~ rR(sK3,sK1,vd1306),
inference(definition_unfolding,[],[f446,f455,f459]) ).
fof(f742,plain,
rR(sK2,sK3,vd1300),
inference(definition_unfolding,[],[f450,f457,f455,f471]) ).
fof(f743,plain,
vf(sK3,sK2) = vf(sK3,sK1),
inference(definition_unfolding,[],[f463,f455,f457,f455,f459]) ).
fof(f744,plain,
sK1 != sK2,
inference(definition_unfolding,[],[f462,f459,f457]) ).
fof(f749,plain,
vd1306 != sK3,
inference(definition_unfolding,[],[f486,f455]) ).
fof(f750,plain,
vf(sK3,vd1300) = vf(sK3,vd1306),
inference(definition_unfolding,[],[f487,f455,f471,f455]) ).
fof(f751,plain,
sK1 != sK3,
inference(definition_unfolding,[],[f488,f459,f455]) ).
fof(f755,plain,
sK2 != sK3,
inference(definition_unfolding,[],[f493,f457,f455]) ).
fof(f762,plain,
ron(sK1,vd1297),
inference(definition_unfolding,[],[f509,f459]) ).
fof(f763,plain,
ron(sK2,vd1295),
inference(definition_unfolding,[],[f510,f457]) ).
fof(f764,plain,
ron(sK3,vd1297),
inference(definition_unfolding,[],[f512,f455]) ).
fof(f766,plain,
ron(sK3,vd1295),
inference(definition_unfolding,[],[f514,f455]) ).
fof(f767,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,[],[f531,f550]) ).
fof(f768,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,[],[f530,f550]) ).
fof(f769,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,[],[f529,f550]) ).
fof(f776,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,[],[f464]) ).
fof(f777,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,[],[f776]) ).
fof(f778,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,[],[f777]) ).
fof(f779,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,[],[f778]) ).
fof(f780,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,[],[f779]) ).
fof(f781,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,[],[f780]) ).
fof(f782,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,[],[f781]) ).
fof(f783,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,[],[f465]) ).
fof(f784,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,[],[f783]) ).
fof(f785,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,[],[f784]) ).
fof(f786,plain,
! [X6,X7,X4,X5] :
( ~ rR(X6,X7,X5)
| ~ rR(X5,X6,X4)
| rR(X6,X7,X4)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f785]) ).
fof(f787,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,[],[f469]) ).
fof(f788,plain,
! [X3,X0,X4,X5] :
( ~ rR(X0,X4,X3)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f787]) ).
fof(f789,plain,
! [X3,X4,X5] :
( ~ rR(X5,X4,X3)
| ~ rR(X4,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f788]) ).
fof(f790,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,[],[f468]) ).
fof(f791,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X3,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f790]) ).
fof(f792,plain,
! [X3,X4,X5] :
( ~ rR(X4,X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f791]) ).
fof(f793,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f792]) ).
fof(f794,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,[],[f467]) ).
fof(f795,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X1,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X1 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f794]) ).
fof(f796,plain,
! [X3,X4,X5] :
( ~ rR(X4,X4,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X4 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f795]) ).
fof(f797,plain,
! [X3,X5] :
( ~ rR(X5,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f796]) ).
fof(f798,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,[],[f466]) ).
fof(f799,plain,
! [X3,X0,X4,X5] :
( rR(X4,X3,X0)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f798]) ).
fof(f800,plain,
! [X3,X4,X5] :
( ~ rR(X4,X5,X3)
| rR(X4,X3,X5)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f799]) ).
fof(f899,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,[],[f508]) ).
fof(f900,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,[],[f899]) ).
fof(f901,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,[],[f900]) ).
fof(f902,plain,
! [X6,X7,X4,X5] :
( ~ rR(X6,X7,X5)
| ~ ron(X6,X4)
| ~ ron(X7,X4)
| ron(X5,X4)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f901]) ).
fof(f909,plain,
! [X3,X0,X4] :
( vf(X0,X3) = sK7(X0,X3)
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f518]) ).
fof(f910,plain,
! [X3,X4] :
( ~ rpoint(X4)
| ~ rpoint(X3)
| vf(X4,X3) = sK7(X4,X3) ),
inference(equality_resolution,[],[f909]) ).
fof(f914,plain,
! [X3,X0,X4] :
( ron(X3,sK8(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f522]) ).
fof(f915,plain,
! [X3,X4] :
( ron(X3,sK8(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f914]) ).
fof(f916,plain,
! [X3,X0,X4] :
( ron(X0,sK8(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f521]) ).
fof(f917,plain,
! [X3,X4] :
( ron(X4,sK8(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f916]) ).
fof(f918,plain,
! [X3,X0,X4] :
( rline(sK8(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f520]) ).
fof(f919,plain,
! [X3,X4] :
( rline(sK8(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f918]) ).
fof(f944,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,[],[f767]) ).
fof(f945,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,[],[f944]) ).
fof(f946,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,[],[f945]) ).
fof(f947,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,[],[f946]) ).
fof(f948,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,[],[f768]) ).
fof(f949,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,[],[f948]) ).
fof(f950,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,[],[f949]) ).
fof(f951,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,[],[f950]) ).
fof(f952,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,[],[f769]) ).
fof(f953,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,[],[f952]) ).
fof(f954,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,[],[f953]) ).
fof(f955,plain,
! [X3,X1,X7,X5] :
( ~ ron(X5,X7)
| rR(X1,X3,X5)
| vd684 = vangle(X3,X1,X5)
| ~ ron(X3,X7)
| ~ ron(X1,X7)
| X1 = X5
| X1 = X3
| ~ rline(X7)
| ~ rpoint(X5)
| ~ rpoint(X3)
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f954]) ).
fof(f962,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,[],[f534]) ).
fof(f963,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,[],[f962]) ).
fof(f964,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,[],[f536]) ).
fof(f965,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,[],[f964]) ).
fof(f966,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,[],[f965]) ).
fof(f994,plain,
! [X2,X3,X0] :
( vf(X0,X2) = vf(X2,X0)
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f546]) ).
fof(f995,plain,
! [X2,X3] :
( ~ rpoint(X3)
| ~ rpoint(X2)
| vf(X3,X2) = vf(X2,X3) ),
inference(equality_resolution,[],[f994]) ).
fof(f1052,plain,
! [X3,X0,X1,X4,X5] :
( vf(X0,X3) = vplus(vf(X0,X1),vf(X1,X3))
| ~ rR(X1,X0,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f572]) ).
fof(f1053,plain,
! [X3,X0,X4,X5] :
( vf(X0,X3) = vplus(vf(X0,X4),vf(X4,X3))
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1052]) ).
fof(f1054,plain,
! [X3,X4,X5] :
( ~ rR(X4,X5,X3)
| vf(X5,X3) = vplus(vf(X5,X4),vf(X4,X3))
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1053]) ).
fof(f1059,plain,
! [X3,X0,X4] :
( ron(X3,sK13(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f577]) ).
fof(f1060,plain,
! [X3,X4] :
( ron(X3,sK13(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1059]) ).
fof(f1061,plain,
! [X3,X0,X4] :
( rcenter(X0,sK13(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f576]) ).
fof(f1062,plain,
! [X3,X4] :
( rcenter(X4,sK13(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1061]) ).
fof(f1063,plain,
! [X3,X0,X4] :
( rcircle(sK13(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f575]) ).
fof(f1064,plain,
! [X3,X4] :
( rcircle(sK13(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f1063]) ).
fof(f1151,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,[],[f605]) ).
fof(f1152,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,[],[f1151]) ).
fof(f1153,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,[],[f1152]) ).
fof(f1154,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,[],[f1153]) ).
fof(f1155,plain,
! [X8,X6,X9,X7,X4] :
( ~ rinside(X9,X6)
| X7 = X8
| ~ ron(X7,X6)
| ~ ron(X8,X6)
| rR(X9,X8,X7)
| ~ ron(X7,X4)
| ~ ron(X8,X4)
| ~ ron(X9,X4)
| ~ rcircle(X6)
| ~ rline(X4)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9) ),
inference(equality_resolution,[],[f1154]) ).
fof(f1546,definition,
sF52 = vf(vd1300,sK1),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f1547,plain,
vf(vd1300,sK1) = sF52,
inference(reorient_equations,[],[f1546]) ).
fof(f1548,definition,
sF53 = vf(vd1306,sK2),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f1549,plain,
vf(vd1306,sK2) = sF53,
inference(reorient_equations,[],[f1548]) ).
fof(f1550,plain,
sF52 != sF53,
inference(definition_folding,[],[f735,f1549,f1547]) ).
fof(f1552,plain,
! [X3,X5] :
( ~ rR(X5,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X5) ),
inference(duplicate_literal_removal,[],[f797]) ).
fof(f1553,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f793]) ).
fof(f1601,plain,
( rR(sK2,vd1300,sK3)
| ~ rpoint(vd1300)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(resolution,[],[f800,f742]) ).
fof(f1604,plain,
( rR(sK2,vd1300,sK3)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1601,f472]) ).
fof(f1606,plain,
( rR(sK2,vd1300,sK3)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1604,f456]) ).
fof(f1608,plain,
rR(sK2,vd1300,sK3),
inference(forward_subsumption_resolution,[],[f1606,f454]) ).
fof(f1615,plain,
! [X0] :
( ~ rpoint(X0)
| vf(vd1306,X0) = vf(X0,vd1306) ),
inference(resolution,[],[f995,f449]) ).
fof(f1616,plain,
! [X0] :
( ~ rpoint(X0)
| vf(vd1300,X0) = vf(X0,vd1300) ),
inference(resolution,[],[f995,f472]) ).
fof(f1618,plain,
! [X0] :
( ~ rpoint(X0)
| vf(sK2,X0) = vf(X0,sK2) ),
inference(resolution,[],[f995,f456]) ).
fof(f1619,plain,
! [X0] :
( ~ rpoint(X0)
| vf(sK3,X0) = vf(X0,sK3) ),
inference(resolution,[],[f995,f454]) ).
fof(f1622,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK3,X0,X1)
| rR(sK3,X2,X3)
| sK3 = X1
| sK3 = X3
| sK3 = X0
| sK3 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1295)
| ~ ron(X2,vd1295)
| vangle(X3,sK3,X1) = vangle(X2,sK3,X0)
| ~ rline(X4)
| ~ rline(vd1295)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK3) ),
inference(resolution,[],[f782,f766]) ).
fof(f1624,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK1,X0,X1)
| rR(sK1,X2,X3)
| sK1 = X1
| sK1 = X3
| sK1 = X0
| sK1 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK1,X1) = vangle(X2,sK1,X0)
| ~ rline(X4)
| ~ rline(vd1297)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK1) ),
inference(resolution,[],[f782,f762]) ).
fof(f1625,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK3,X0,X1)
| rR(sK3,X2,X3)
| sK3 = X1
| sK3 = X3
| sK3 = X0
| sK3 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK3,X1) = vangle(X2,sK3,X0)
| ~ rline(X4)
| ~ rline(vd1297)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK3) ),
inference(resolution,[],[f782,f764]) ).
fof(f1665,plain,
vf(vd1300,sK1) = vf(sK1,vd1300),
inference(resolution,[],[f1616,f458]) ).
fof(f1668,plain,
sF52 = vf(sK1,vd1300),
inference(forward_demodulation,[],[f1665,f1547]) ).
fof(f1675,plain,
vf(vd1306,sK2) = vf(sK2,vd1306),
inference(resolution,[],[f1615,f456]) ).
fof(f1678,plain,
sF53 = vf(sK2,vd1306),
inference(forward_demodulation,[],[f1675,f1549]) ).
fof(f1747,plain,
! [X0] :
( ~ rR(sK3,sK2,X0)
| rR(sK2,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rpoint(vd1300) ),
inference(resolution,[],[f786,f1608]) ).
fof(f1752,plain,
! [X0] :
( ~ rR(sK3,sK2,X0)
| rR(sK2,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(sK2)
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f1747,f454]) ).
fof(f1758,plain,
! [X0] :
( ~ rR(sK3,sK2,X0)
| rR(sK2,vd1300,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1300) ),
inference(forward_subsumption_resolution,[],[f1752,f456]) ).
fof(f1764,plain,
! [X0] :
( ~ rR(sK3,sK2,X0)
| rR(sK2,vd1300,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1758,f472]) ).
fof(f1773,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK2 = X1
| ~ rpoint(X0)
| sK2 = X0
| vangle(X0,X1,sK2) = vangle(sK2,X1,X0) ),
inference(resolution,[],[f966,f456]) ).
fof(f1782,plain,
vf(sK3,sK2) = vf(sK2,sK3),
inference(resolution,[],[f1618,f454]) ).
fof(f1783,plain,
vf(sK3,sK1) = vf(sK2,sK3),
inference(forward_demodulation,[],[f1782,f743]) ).
fof(f1789,plain,
vf(sK3,sK1) = vf(sK1,sK3),
inference(resolution,[],[f1619,f458]) ).
fof(f2028,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X0)
| vd684 = vangle(X3,X2,X0)
| ~ ron(X3,sK8(X1,X0))
| ~ ron(X2,sK8(X1,X0))
| X0 = X2
| X2 = X3
| ~ rline(sK8(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(resolution,[],[f915,f955]) ).
fof(f2031,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X0)
| vd684 = vangle(X3,X2,X0)
| ~ ron(X3,sK8(X1,X0))
| ~ ron(X2,sK8(X1,X0))
| X0 = X2
| X2 = X3
| ~ rline(sK8(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f2028]) ).
fof(f2034,plain,
! [X2,X3,X0,X1] :
( ~ ron(X3,sK8(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X3,X0)
| vd684 = vangle(X3,X2,X0)
| X0 = X1
| ~ ron(X2,sK8(X1,X0))
| X0 = X2
| X2 = X3
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f2031,f919]) ).
fof(f2036,plain,
! [X2,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X0,X0)
| vd684 = vangle(X0,X2,X0)
| X0 = X1
| ~ ron(X2,sK8(X1,X0))
| X0 = X2
| X0 = X2
| ~ rpoint(X0)
| ~ rpoint(X2)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f2034,f915]) ).
fof(f2037,plain,
! [X2,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X2,X0,X0)
| vd684 = vangle(X0,X2,X0)
| X0 = X1
| ~ ron(X2,sK8(X1,X0))
| X0 = X2
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f2036]) ).
fof(f2038,plain,
! [X2,X0,X1] :
( ~ ron(X2,sK8(X1,X0))
| ~ rpoint(X1)
| vd684 = vangle(X0,X2,X0)
| X0 = X1
| ~ rpoint(X0)
| X0 = X2
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f2037,f1553]) ).
fof(f2041,plain,
! [X0,X1] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rpoint(X1)
| vd684 = vangle(X0,X1,X0)
| X0 = X1
| ~ rpoint(X0)
| X0 = X1
| ~ rpoint(X1) ),
inference(resolution,[],[f917,f2038]) ).
fof(f2045,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X1,X2,X3)
| rR(X1,X4,X5)
| X1 = X3
| X1 = X5
| X1 = X2
| X1 = X4
| ~ ron(X3,X6)
| ~ ron(X2,X6)
| ~ ron(X5,sK8(X1,X0))
| ~ ron(X4,sK8(X1,X0))
| vangle(X5,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X6)
| ~ rline(sK8(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1) ),
inference(resolution,[],[f917,f782]) ).
fof(f2046,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X1,X2,X3)
| rR(X1,X4,X5)
| X1 = X3
| X1 = X5
| X1 = X2
| X1 = X4
| ~ ron(X3,X6)
| ~ ron(X2,X6)
| ~ ron(X5,sK8(X1,X0))
| ~ ron(X4,sK8(X1,X0))
| vangle(X5,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X6)
| ~ rline(sK8(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f2045]) ).
fof(f2050,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X1
| vd684 = vangle(X0,X1,X0) ),
inference(duplicate_literal_removal,[],[f2041]) ).
fof(f2051,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ ron(X5,sK8(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X1,X2,X3)
| rR(X1,X4,X5)
| X1 = X3
| X1 = X5
| X1 = X2
| X1 = X4
| ~ ron(X3,X6)
| ~ ron(X2,X6)
| X0 = X1
| ~ ron(X4,sK8(X1,X0))
| vangle(X5,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X6)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(forward_subsumption_resolution,[],[f2046,f919]) ).
fof(f2057,plain,
! [X0] :
( ~ rpoint(X0)
| sK1 = X0
| vd684 = vangle(X0,sK1,X0) ),
inference(resolution,[],[f2050,f458]) ).
fof(f2059,plain,
! [X0] :
( ~ rpoint(X0)
| sK3 = X0
| vd684 = vangle(X0,sK3,X0) ),
inference(resolution,[],[f2050,f454]) ).
fof(f2068,plain,
( vd1306 = sK3
| vd684 = vangle(vd1306,sK3,vd1306) ),
inference(resolution,[],[f2059,f449]) ).
fof(f2072,plain,
( sK2 = sK3
| vd684 = vangle(sK2,sK3,sK2) ),
inference(resolution,[],[f2059,f456]) ).
fof(f2074,plain,
vd684 = vangle(sK2,sK3,sK2),
inference(forward_subsumption_resolution,[],[f2072,f755]) ).
fof(f2078,plain,
vd684 = vangle(vd1306,sK3,vd1306),
inference(forward_subsumption_resolution,[],[f2068,f749]) ).
fof(f2149,plain,
( sK1 = sK2
| vd684 = vangle(sK2,sK1,sK2) ),
inference(resolution,[],[f2057,f456]) ).
fof(f2150,plain,
( sK1 = sK3
| vd684 = vangle(sK3,sK1,sK3) ),
inference(resolution,[],[f2057,f454]) ).
fof(f2151,plain,
vd684 = vangle(sK3,sK1,sK3),
inference(forward_subsumption_resolution,[],[f2150,f751]) ).
fof(f2152,plain,
vd684 = vangle(sK2,sK1,sK2),
inference(forward_subsumption_resolution,[],[f2149,f744]) ).
fof(f2831,plain,
! [X0,X1] :
( vf(sK3,sK1) != vf(sK3,X0)
| ron(sK2,X1)
| ~ ron(X0,X1)
| ~ rpoint(X0)
| ~ rcenter(sK3,X1)
| ~ rpoint(sK2) ),
inference(superposition,[],[f963,f743]) ).
fof(f2845,plain,
! [X0,X1] :
( vf(sK3,sK1) != vf(sK3,X0)
| ron(X0,X1)
| ~ ron(sK2,X1)
| ~ rpoint(sK2)
| ~ rcenter(sK3,X1)
| ~ rpoint(X0) ),
inference(superposition,[],[f963,f743]) ).
fof(f2850,plain,
! [X0,X1] :
( vf(sK3,sK1) != vf(sK3,X0)
| ron(X0,X1)
| ~ ron(sK2,X1)
| ~ rcenter(sK3,X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2845,f456]) ).
fof(f2863,plain,
! [X0,X1] :
( vf(sK3,sK1) != vf(sK3,X0)
| ron(sK2,X1)
| ~ ron(X0,X1)
| ~ rpoint(X0)
| ~ rcenter(sK3,X1) ),
inference(forward_subsumption_resolution,[],[f2831,f456]) ).
fof(f2901,plain,
! [X0] :
( sK1 = sK2
| ~ rpoint(X0)
| sK2 = X0
| vangle(X0,sK1,sK2) = vangle(sK2,sK1,X0) ),
inference(resolution,[],[f1773,f458]) ).
fof(f2903,plain,
! [X0] :
( sK2 = sK3
| ~ rpoint(X0)
| sK2 = X0
| vangle(X0,sK3,sK2) = vangle(sK2,sK3,X0) ),
inference(resolution,[],[f1773,f454]) ).
fof(f2904,plain,
! [X0] :
( ~ rpoint(X0)
| sK2 = X0
| vangle(X0,sK3,sK2) = vangle(sK2,sK3,X0) ),
inference(forward_subsumption_resolution,[],[f2903,f755]) ).
fof(f2905,plain,
! [X0] :
( ~ rpoint(X0)
| sK2 = X0
| vangle(X0,sK1,sK2) = vangle(sK2,sK1,X0) ),
inference(forward_subsumption_resolution,[],[f2901,f744]) ).
fof(f3143,plain,
( sK2 = sK3
| vangle(sK3,sK1,sK2) = vangle(sK2,sK1,sK3) ),
inference(resolution,[],[f2905,f454]) ).
fof(f3144,plain,
vangle(sK3,sK1,sK2) = vangle(sK2,sK1,sK3),
inference(forward_subsumption_resolution,[],[f3143,f755]) ).
fof(f3153,plain,
( sK1 = sK2
| vangle(sK2,sK3,sK1) = vangle(sK1,sK3,sK2) ),
inference(resolution,[],[f2904,f458]) ).
fof(f3157,plain,
vangle(sK2,sK3,sK1) = vangle(sK1,sK3,sK2),
inference(forward_subsumption_resolution,[],[f3153,f744]) ).
fof(f3192,plain,
! [X0] :
( vd684 != vangle(sK3,sK1,sK2)
| ron(sK3,X0)
| ~ ron(sK2,X0)
| ~ ron(sK1,X0)
| sK1 = sK3
| sK1 = sK2
| ~ rline(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rpoint(sK1) ),
inference(superposition,[],[f951,f3144]) ).
fof(f3265,plain,
! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ~ rR(sK3,sK2,sK1)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| sK2 = sK3
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(superposition,[],[f947,f3157]) ).
fof(f4965,plain,
! [X0] :
( ron(sK1,X0)
| ~ ron(sK2,X0)
| ~ rcenter(sK3,X0)
| ~ rpoint(sK1) ),
inference(equality_resolution,[],[f2850]) ).
fof(f4968,plain,
! [X0] :
( ~ rcenter(sK3,X0)
| ~ ron(sK2,X0)
| ron(sK1,X0) ),
inference(forward_subsumption_resolution,[],[f4965,f458]) ).
fof(f5635,plain,
! [X0] :
( ~ rpoint(X0)
| vf(sK2,X0) = sK7(sK2,X0) ),
inference(resolution,[],[f910,f456]) ).
fof(f5636,plain,
! [X0] :
( ~ rpoint(X0)
| vf(sK3,X0) = sK7(sK3,X0) ),
inference(resolution,[],[f910,f454]) ).
fof(f5652,plain,
vf(sK2,sK3) = sK7(sK2,sK3),
inference(resolution,[],[f5635,f454]) ).
fof(f5653,plain,
vf(sK3,sK1) = sK7(sK2,sK3),
inference(forward_demodulation,[],[f5652,f1783]) ).
fof(f5678,plain,
vf(sK3,vd1300) = sK7(sK3,vd1300),
inference(resolution,[],[f5636,f472]) ).
fof(f5685,plain,
vf(sK3,sK1) = sK7(sK3,sK1),
inference(resolution,[],[f5636,f458]) ).
fof(f5690,plain,
sK7(sK2,sK3) = sK7(sK3,sK1),
inference(forward_demodulation,[],[f5685,f5653]) ).
fof(f5885,plain,
! [X0] :
( ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ rpoint(sK1)
| ~ rcenter(sK3,X0) ),
inference(equality_resolution,[],[f2863]) ).
fof(f5891,plain,
! [X0] :
( ~ rcenter(sK3,X0)
| ~ ron(sK1,X0)
| ron(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f5885,f458]) ).
fof(f6125,plain,
! [X0] :
( sK3 = X0
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ ron(sK1,sK13(sK3,X0))
| ron(sK2,sK13(sK3,X0)) ),
inference(resolution,[],[f1062,f5891]) ).
fof(f6127,plain,
! [X0] :
( sK3 = X0
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ ron(sK2,sK13(sK3,X0))
| ron(sK1,sK13(sK3,X0)) ),
inference(resolution,[],[f1062,f4968]) ).
fof(f6132,plain,
! [X0] :
( ~ ron(sK2,sK13(sK3,X0))
| ~ rpoint(X0)
| sK3 = X0
| ron(sK1,sK13(sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f6127,f454]) ).
fof(f6134,plain,
! [X0] :
( ~ ron(sK1,sK13(sK3,X0))
| ~ rpoint(X0)
| sK3 = X0
| ron(sK2,sK13(sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f6125,f454]) ).
fof(f6145,plain,
( ~ rpoint(sK1)
| sK1 = sK3
| ron(sK2,sK13(sK3,sK1))
| sK1 = sK3
| ~ rpoint(sK1)
| ~ rpoint(sK3) ),
inference(resolution,[],[f6134,f1060]) ).
fof(f6146,plain,
( ~ rpoint(sK1)
| sK1 = sK3
| ron(sK2,sK13(sK3,sK1))
| ~ rpoint(sK3) ),
inference(duplicate_literal_removal,[],[f6145]) ).
fof(f6147,plain,
( sK1 = sK3
| ron(sK2,sK13(sK3,sK1))
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f6146,f458]) ).
fof(f6149,plain,
( ron(sK2,sK13(sK3,sK1))
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f6147,f751]) ).
fof(f6151,plain,
ron(sK2,sK13(sK3,sK1)),
inference(forward_subsumption_resolution,[],[f6149,f454]) ).
fof(f6157,plain,
( ~ rpoint(sK1)
| sK1 = sK3
| ron(sK1,sK13(sK3,sK1)) ),
inference(resolution,[],[f6151,f6132]) ).
fof(f6162,plain,
( sK1 = sK3
| ron(sK1,sK13(sK3,sK1)) ),
inference(forward_subsumption_resolution,[],[f6157,f458]) ).
fof(f6163,plain,
ron(sK1,sK13(sK3,sK1)),
inference(forward_subsumption_resolution,[],[f6162,f751]) ).
fof(f10307,plain,
! [X0,X1] :
( rinside(X0,sK13(X0,X1))
| X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f574,f1062]) ).
fof(f10310,plain,
! [X2,X3,X0,X1,X4] :
( X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0)
| X2 = X3
| ~ ron(X2,sK13(X0,X1))
| ~ ron(X3,sK13(X0,X1))
| rR(X0,X3,X2)
| ~ ron(X2,X4)
| ~ ron(X3,X4)
| ~ ron(X0,X4)
| ~ rcircle(sK13(X0,X1))
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X0) ),
inference(resolution,[],[f10307,f1155]) ).
fof(f10312,plain,
! [X2,X3,X0,X1,X4] :
( X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0)
| X2 = X3
| ~ ron(X2,sK13(X0,X1))
| ~ ron(X3,sK13(X0,X1))
| rR(X0,X3,X2)
| ~ ron(X2,X4)
| ~ ron(X3,X4)
| ~ ron(X0,X4)
| ~ rcircle(sK13(X0,X1))
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X3) ),
inference(duplicate_literal_removal,[],[f10310]) ).
fof(f10313,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,sK13(X0,X1))
| ~ rpoint(X1)
| ~ rpoint(X0)
| X2 = X3
| ~ ron(X2,sK13(X0,X1))
| X0 = X1
| rR(X0,X3,X2)
| ~ ron(X2,X4)
| ~ ron(X3,X4)
| ~ ron(X0,X4)
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X3) ),
inference(forward_subsumption_resolution,[],[f10312,f1064]) ).
fof(f22457,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK3,X0,X1)
| rR(sK3,X2,X3)
| sK3 = X1
| sK3 = X3
| sK3 = X0
| sK3 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK3,X1) = vangle(X2,sK3,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1625,f498]) ).
fof(f22458,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK1,X0,X1)
| rR(sK1,X2,X3)
| sK1 = X1
| sK1 = X3
| sK1 = X0
| sK1 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1297)
| ~ ron(X2,vd1297)
| vangle(X3,sK1,X1) = vangle(X2,sK1,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f1624,f498]) ).
fof(f22460,plain,
! [X2,X3,X0,X1,X4] :
( rR(sK3,X0,X1)
| rR(sK3,X2,X3)
| sK3 = X1
| sK3 = X3
| sK3 = X0
| sK3 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ ron(X3,vd1295)
| ~ ron(X2,vd1295)
| vangle(X3,sK3,X1) = vangle(X2,sK3,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1622,f501]) ).
fof(f22503,plain,
! [X0] :
( vd684 != vangle(sK3,sK1,sK2)
| ron(sK3,X0)
| ~ ron(sK2,X0)
| ~ ron(sK1,X0)
| sK1 = sK2
| ~ rline(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f3192,f751]) ).
fof(f23165,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,vd1297)
| rR(sK3,X2,X3)
| sK3 = X1
| sK3 = X3
| sK3 = X0
| sK3 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| rR(sK3,X0,X1)
| ~ ron(X2,vd1297)
| vangle(X3,sK3,X1) = vangle(X2,sK3,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f22457,f454]) ).
fof(f23166,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,vd1297)
| rR(sK1,X2,X3)
| sK1 = X1
| sK1 = X3
| sK1 = X0
| sK1 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| rR(sK1,X0,X1)
| ~ ron(X2,vd1297)
| vangle(X3,sK1,X1) = vangle(X2,sK1,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f22458,f458]) ).
fof(f23168,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,vd1295)
| rR(sK3,X2,X3)
| sK3 = X1
| sK3 = X3
| sK3 = X0
| sK3 = X2
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| rR(sK3,X0,X1)
| ~ ron(X2,vd1295)
| vangle(X3,sK3,X1) = vangle(X2,sK3,X0)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f22460,f454]) ).
fof(f23209,plain,
! [X0] :
( vd684 != vangle(sK3,sK1,sK2)
| ron(sK3,X0)
| ~ ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f22503,f744]) ).
fof(f23483,plain,
! [X0] :
( vd684 != vangle(sK3,sK1,sK2)
| ron(sK3,X0)
| ~ ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f23209,f454]) ).
fof(f23673,plain,
! [X0] :
( vd684 != vangle(sK3,sK1,sK2)
| ron(sK3,X0)
| ~ ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f23483,f456]) ).
fof(f24074,definition,
( spl54_804
<=> ! [X0] :
( ~ ron(sK1,X0)
| ~ rline(X0)
| ~ ron(sK3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_804])],[avatar_definition]) ).
fof(f24075,plain,
( ! [X0] :
( ~ ron(sK3,X0)
| ~ rline(X0)
| ~ ron(sK1,X0) )
| ~ spl54_804 ),
inference(avatar_component_clause,[],[f24074]) ).
fof(f24077,definition,
( spl54_805
<=> rR(sK3,sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl54_805])],[avatar_definition]) ).
fof(f24078,plain,
( rR(sK3,sK1,sK2)
| ~ spl54_805 ),
inference(avatar_component_clause,[],[f24077]) ).
fof(f24079,plain,
( ~ rR(sK3,sK1,sK2)
| spl54_805 ),
inference(avatar_component_clause,[],[f24077]) ).
fof(f24241,definition,
( spl54_818
<=> ! [X0] :
( ~ ron(sK1,X0)
| ~ rline(X0)
| ~ ron(sK2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_818])],[avatar_definition]) ).
fof(f24242,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ rline(X0)
| ~ ron(sK2,X0) )
| ~ spl54_818 ),
inference(avatar_component_clause,[],[f24241]) ).
fof(f24396,definition,
( spl54_832
<=> ! [X0] :
( ~ ron(sK2,X0)
| ~ rline(X0)
| ~ ron(sK3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_832])],[avatar_definition]) ).
fof(f24397,plain,
( ! [X0] :
( ~ ron(sK2,X0)
| ~ rline(X0)
| ~ ron(sK3,X0) )
| ~ spl54_832 ),
inference(avatar_component_clause,[],[f24396]) ).
fof(f24399,definition,
( spl54_833
<=> rR(sK3,sK2,vd1306) ),
introduced(definition,[new_symbols(definition,[spl54_833])],[avatar_definition]) ).
fof(f24400,plain,
( rR(sK3,sK2,vd1306)
| ~ spl54_833 ),
inference(avatar_component_clause,[],[f24399]) ).
fof(f24401,plain,
( ~ rR(sK3,sK2,vd1306)
| spl54_833 ),
inference(avatar_component_clause,[],[f24399]) ).
fof(f26499,plain,
! [X2,X3,X0,X1] :
( rR(sK1,X0,sK3)
| sK1 = X1
| sK1 = sK3
| sK1 = X2
| sK1 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK1,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK1,X2) = vangle(sK3,sK1,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK3)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f23166,f764]) ).
fof(f26505,plain,
! [X2,X3,X0,X1] :
( rR(sK1,X0,sK3)
| sK1 = X1
| sK1 = X2
| sK1 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK1,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK1,X2) = vangle(sK3,sK1,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK3)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26499,f751]) ).
fof(f26510,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,X3)
| sK1 = X1
| sK1 = X2
| sK1 = X0
| ~ ron(X1,X3)
| rR(sK1,X0,sK3)
| rR(sK1,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK1,X2) = vangle(sK3,sK1,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26505,f454]) ).
fof(f26514,definition,
( spl54_927
<=> ron(sK2,vd1297) ),
introduced(definition,[new_symbols(definition,[spl54_927])],[avatar_definition]) ).
fof(f26515,plain,
( ron(sK2,vd1297)
| ~ spl54_927 ),
inference(avatar_component_clause,[],[f26514]) ).
fof(f26516,plain,
( ~ ron(sK2,vd1297)
| spl54_927 ),
inference(avatar_component_clause,[],[f26514]) ).
fof(f26617,definition,
( spl54_931
<=> vd684 = vangle(sK3,sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl54_931])],[avatar_definition]) ).
fof(f26618,plain,
( vd684 != vangle(sK3,sK1,sK2)
| spl54_931 ),
inference(avatar_component_clause,[],[f26617]) ).
fof(f26619,plain,
( vd684 = vangle(sK3,sK1,sK2)
| ~ spl54_931 ),
inference(avatar_component_clause,[],[f26617]) ).
fof(f26700,plain,
! [X2,X3,X0,X1] :
( rR(sK3,X0,sK2)
| sK3 = X1
| sK2 = sK3
| sK3 = X2
| sK3 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK3,X2,X1)
| ~ ron(X0,vd1295)
| vangle(X0,sK3,X2) = vangle(sK2,sK3,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK2)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f23168,f763]) ).
fof(f26705,plain,
! [X2,X3,X0,X1] :
( rR(sK3,X0,sK2)
| sK3 = X1
| sK3 = X2
| sK3 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK3,X2,X1)
| ~ ron(X0,vd1295)
| vangle(X0,sK3,X2) = vangle(sK2,sK3,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(sK2)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26700,f755]) ).
fof(f26708,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,X3)
| sK3 = X1
| sK3 = X2
| sK3 = X0
| ~ ron(X1,X3)
| rR(sK3,X0,sK2)
| rR(sK3,X2,X1)
| ~ ron(X0,vd1295)
| vangle(X0,sK3,X2) = vangle(sK2,sK3,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26705,f456]) ).
fof(f26713,plain,
! [X2,X3,X0,X1] :
( rR(sK3,X0,vd1306)
| sK3 = X1
| vd1306 = sK3
| sK3 = X2
| sK3 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK3,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK3,X2) = vangle(vd1306,sK3,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(vd1306)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f23165,f511]) ).
fof(f26722,plain,
! [X2,X3,X0,X1] :
( rR(sK3,X0,vd1306)
| sK3 = X1
| sK3 = X2
| sK3 = X0
| ~ ron(X1,X3)
| ~ ron(X2,X3)
| rR(sK3,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK3,X2) = vangle(vd1306,sK3,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(vd1306)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26713,f749]) ).
fof(f26725,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,X3)
| sK3 = X1
| sK3 = X2
| sK3 = X0
| ~ ron(X1,X3)
| rR(sK3,X0,vd1306)
| rR(sK3,X2,X1)
| ~ ron(X0,vd1297)
| vangle(X0,sK3,X2) = vangle(vd1306,sK3,X1)
| ~ rline(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f26722,f449]) ).
fof(f26736,plain,
! [X0,X1] :
( sK1 = X0
| sK1 = sK3
| sK1 = X1
| ~ ron(X0,vd1295)
| rR(sK1,X1,sK3)
| rR(sK1,sK3,X0)
| ~ ron(X1,vd1297)
| vangle(sK3,sK1,X0) = vangle(X1,sK1,sK3)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(X1) ),
inference(resolution,[],[f26510,f766]) ).
fof(f26754,plain,
! [X0,X1] :
( sK1 = X0
| sK1 = X1
| ~ ron(X0,vd1295)
| rR(sK1,X1,sK3)
| rR(sK1,sK3,X0)
| ~ ron(X1,vd1297)
| vangle(sK3,sK1,X0) = vangle(X1,sK1,sK3)
| ~ rline(vd1295)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26736,f751]) ).
fof(f26763,plain,
! [X0,X1] :
( sK1 = X0
| sK1 = X1
| ~ ron(X0,vd1295)
| rR(sK1,X1,sK3)
| rR(sK1,sK3,X0)
| ~ ron(X1,vd1297)
| vangle(sK3,sK1,X0) = vangle(X1,sK1,sK3)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26754,f501]) ).
fof(f26772,plain,
! [X0,X1] :
( rR(sK1,sK3,X0)
| rR(sK1,X1,sK3)
| ~ ron(X0,vd1295)
| sK1 = X1
| sK1 = X0
| ~ ron(X1,vd1297)
| vangle(sK3,sK1,X0) = vangle(X1,sK1,sK3)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f26763,f454]) ).
fof(f26880,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X1,X2,X3)
| rR(X1,X4,X0)
| X1 = X3
| X0 = X1
| X1 = X2
| X1 = X4
| ~ ron(X3,X5)
| ~ ron(X2,X5)
| X0 = X1
| ~ ron(X4,sK8(X1,X0))
| vangle(X0,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X5)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(X4)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f2051,f915]) ).
fof(f26886,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ ron(X4,sK8(X1,X0))
| ~ rpoint(X1)
| rR(X1,X2,X3)
| rR(X1,X4,X0)
| X1 = X3
| X0 = X1
| X1 = X2
| X1 = X4
| ~ ron(X3,X5)
| ~ ron(X2,X5)
| ~ rpoint(X0)
| vangle(X0,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X5)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f26880]) ).
fof(f27046,definition,
( spl54_935
<=> rR(sK1,sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl54_935])],[avatar_definition]) ).
fof(f27047,plain,
( rR(sK1,sK3,sK2)
| ~ spl54_935 ),
inference(avatar_component_clause,[],[f27046]) ).
fof(f27048,plain,
( ~ rR(sK1,sK3,sK2)
| spl54_935 ),
inference(avatar_component_clause,[],[f27046]) ).
fof(f27171,plain,
! [X2,X3,X0,X1] :
( sK3 = X0
| sK3 = X1
| sK3 = X2
| ~ ron(X0,sK8(X3,X1))
| rR(sK3,X2,sK2)
| rR(sK3,X1,X0)
| ~ ron(X2,vd1295)
| vangle(sK2,sK3,X0) = vangle(X2,sK3,X1)
| ~ rline(sK8(X3,X1))
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rpoint(X2)
| X1 = X3
| ~ rpoint(X1)
| ~ rpoint(X3) ),
inference(resolution,[],[f26708,f915]) ).
fof(f27183,plain,
! [X2,X3,X0,X1] :
( sK3 = X0
| sK3 = X1
| sK3 = X2
| ~ ron(X0,sK8(X3,X1))
| rR(sK3,X2,sK2)
| rR(sK3,X1,X0)
| ~ ron(X2,vd1295)
| vangle(sK2,sK3,X0) = vangle(X2,sK3,X1)
| ~ rline(sK8(X3,X1))
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rpoint(X2)
| X1 = X3
| ~ rpoint(X3) ),
inference(duplicate_literal_removal,[],[f27171]) ).
fof(f27189,plain,
! [X2,X3,X0,X1] :
( ~ ron(X0,sK8(X3,X1))
| sK3 = X1
| sK3 = X2
| sK3 = X0
| rR(sK3,X2,sK2)
| rR(sK3,X1,X0)
| ~ ron(X2,vd1295)
| vangle(sK2,sK3,X0) = vangle(X2,sK3,X1)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rpoint(X2)
| X1 = X3
| ~ rpoint(X3) ),
inference(forward_subsumption_resolution,[],[f27183,f919]) ).
fof(f27343,plain,
! [X0,X1] :
( sK3 = X0
| sK1 = sK3
| sK3 = X1
| ~ ron(X0,vd1297)
| rR(sK3,X1,vd1306)
| rR(sK3,sK1,X0)
| ~ ron(X1,vd1297)
| vangle(vd1306,sK3,X0) = vangle(X1,sK3,sK1)
| ~ rline(vd1297)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(X1) ),
inference(resolution,[],[f26725,f762]) ).
fof(f27371,plain,
! [X0,X1] :
( sK3 = X0
| sK3 = X1
| ~ ron(X0,vd1297)
| rR(sK3,X1,vd1306)
| rR(sK3,sK1,X0)
| ~ ron(X1,vd1297)
| vangle(vd1306,sK3,X0) = vangle(X1,sK3,sK1)
| ~ rline(vd1297)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f27343,f751]) ).
fof(f27384,plain,
! [X0,X1] :
( sK3 = X0
| sK3 = X1
| ~ ron(X0,vd1297)
| rR(sK3,X1,vd1306)
| rR(sK3,sK1,X0)
| ~ ron(X1,vd1297)
| vangle(vd1306,sK3,X0) = vangle(X1,sK3,sK1)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f27371,f498]) ).
fof(f27397,plain,
! [X0,X1] :
( rR(sK3,sK1,X0)
| rR(sK3,X1,vd1306)
| ~ ron(X0,vd1297)
| sK3 = X1
| sK3 = X0
| ~ ron(X1,vd1297)
| vangle(vd1306,sK3,X0) = vangle(X1,sK3,sK1)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f27384,f458]) ).
fof(f27773,plain,
! [X2,X3,X0,X1,X4] :
( ~ rpoint(X0)
| rR(X0,X1,X2)
| rR(X0,X3,X3)
| X0 = X2
| X0 = X3
| X0 = X1
| X0 = X3
| ~ ron(X2,X4)
| ~ ron(X1,X4)
| ~ rpoint(X3)
| vangle(X3,X0,X2) = vangle(X3,X0,X1)
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X3)
| X0 = X3
| ~ rpoint(X3)
| ~ rpoint(X0) ),
inference(resolution,[],[f26886,f915]) ).
fof(f27779,plain,
! [X2,X3,X0,X1,X4] :
( ~ rpoint(X0)
| rR(X0,X1,X2)
| rR(X0,X3,X3)
| X0 = X2
| X0 = X3
| X0 = X1
| ~ ron(X2,X4)
| ~ ron(X1,X4)
| ~ rpoint(X3)
| vangle(X3,X0,X2) = vangle(X3,X0,X1)
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(duplicate_literal_removal,[],[f27773]) ).
fof(f27783,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X2,X4)
| rR(X0,X1,X2)
| X0 = X2
| X0 = X3
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,X4)
| ~ rpoint(X3)
| vangle(X3,X0,X2) = vangle(X3,X0,X1)
| ~ rline(X4)
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f27779,f1553]) ).
fof(f27799,plain,
! [X2,X0,X1] :
( rR(X0,X1,sK2)
| sK2 = X0
| X0 = X2
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,vd1295)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,sK2)
| ~ rline(vd1295)
| ~ rpoint(sK2)
| ~ rpoint(X1) ),
inference(resolution,[],[f27783,f763]) ).
fof(f27821,plain,
! [X2,X0,X1] :
( rR(X0,X1,sK2)
| sK2 = X0
| X0 = X2
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,vd1295)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,sK2)
| ~ rpoint(sK2)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f27799,f501]) ).
fof(f27836,plain,
! [X2,X0,X1] :
( ~ ron(X1,vd1295)
| sK2 = X0
| X0 = X2
| X0 = X1
| ~ rpoint(X0)
| rR(X0,X1,sK2)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,sK2)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f27821,f456]) ).
fof(f28464,plain,
! [X2,X0,X1] :
( sK3 = X0
| sK3 = X1
| sK3 = X2
| rR(sK3,X1,sK2)
| rR(sK3,X0,X2)
| ~ ron(X1,vd1295)
| vangle(X1,sK3,X0) = vangle(sK2,sK3,X2)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X2
| ~ rpoint(X2)
| X0 = X2
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(resolution,[],[f27189,f917]) ).
fof(f28468,plain,
! [X2,X0,X1] :
( rR(sK3,X1,sK2)
| rR(sK3,X0,X2)
| sK3 = X2
| sK3 = X1
| sK3 = X0
| ~ ron(X1,vd1295)
| vangle(X1,sK3,X0) = vangle(sK2,sK3,X2)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X2 ),
inference(duplicate_literal_removal,[],[f28464]) ).
fof(f30227,plain,
! [X0] :
( rR(sK1,sK3,X0)
| ~ ron(X0,vd1295)
| sK1 = sK3
| sK1 = X0
| ~ ron(sK3,vd1297)
| vangle(sK3,sK1,sK3) = vangle(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(resolution,[],[f26772,f1553]) ).
fof(f30230,plain,
! [X0] :
( rR(sK1,sK3,X0)
| ~ ron(X0,vd1295)
| sK1 = sK3
| sK1 = X0
| ~ ron(sK3,vd1297)
| vangle(sK3,sK1,sK3) = vangle(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(duplicate_literal_removal,[],[f30227]) ).
fof(f30254,plain,
! [X0] :
( rR(sK1,sK3,X0)
| ~ ron(X0,vd1295)
| sK1 = X0
| ~ ron(sK3,vd1297)
| vangle(sK3,sK1,sK3) = vangle(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f30230,f751]) ).
fof(f30279,plain,
! [X0] :
( rR(sK1,sK3,X0)
| ~ ron(X0,vd1295)
| sK1 = X0
| vangle(sK3,sK1,sK3) = vangle(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f30254,f764]) ).
fof(f30304,plain,
! [X0] :
( rR(sK1,sK3,X0)
| ~ ron(X0,vd1295)
| sK1 = X0
| vangle(sK3,sK1,sK3) = vangle(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f30279,f454]) ).
fof(f30313,plain,
! [X0] :
( rR(sK1,sK3,X0)
| ~ ron(X0,vd1295)
| sK1 = X0
| vangle(sK3,sK1,sK3) = vangle(sK3,sK1,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f30304,f458]) ).
fof(f30322,plain,
! [X0] :
( rR(sK1,sK3,X0)
| vd684 = vangle(sK3,sK1,X0)
| ~ ron(X0,vd1295)
| sK1 = X0
| ~ rpoint(X0) ),
inference(forward_demodulation,[],[f30313,f2151]) ).
fof(f30331,plain,
( vd684 = vangle(sK3,sK1,sK2)
| ~ ron(sK2,vd1295)
| sK1 = sK2
| ~ rpoint(sK2)
| spl54_935 ),
inference(resolution,[],[f30322,f27048]) ).
fof(f30744,plain,
! [X0] :
( rR(sK3,X0,vd1306)
| ~ ron(vd1306,vd1297)
| sK3 = X0
| vd1306 = sK3
| ~ ron(X0,vd1297)
| vangle(vd1306,sK3,vd1306) = vangle(X0,sK3,sK1)
| ~ rpoint(vd1306)
| ~ rpoint(X0) ),
inference(resolution,[],[f27397,f738]) ).
fof(f30829,plain,
! [X0] :
( rR(sK3,X0,vd1306)
| sK3 = X0
| vd1306 = sK3
| ~ ron(X0,vd1297)
| vangle(vd1306,sK3,vd1306) = vangle(X0,sK3,sK1)
| ~ rpoint(vd1306)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f30744,f511]) ).
fof(f30861,plain,
! [X0] :
( rR(sK3,X0,vd1306)
| sK3 = X0
| ~ ron(X0,vd1297)
| vangle(vd1306,sK3,vd1306) = vangle(X0,sK3,sK1)
| ~ rpoint(vd1306)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f30829,f749]) ).
fof(f30877,plain,
! [X0] :
( rR(sK3,X0,vd1306)
| sK3 = X0
| ~ ron(X0,vd1297)
| vangle(vd1306,sK3,vd1306) = vangle(X0,sK3,sK1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f30861,f449]) ).
fof(f30893,plain,
! [X0] :
( rR(sK3,X0,vd1306)
| vd684 = vangle(X0,sK3,sK1)
| sK3 = X0
| ~ ron(X0,vd1297)
| ~ rpoint(X0) ),
inference(forward_demodulation,[],[f30877,f2078]) ).
fof(f30916,plain,
( vd684 = vangle(sK2,sK3,sK1)
| sK2 = sK3
| ~ ron(sK2,vd1297)
| ~ rpoint(sK2)
| spl54_833 ),
inference(resolution,[],[f30893,f24401]) ).
fof(f30960,plain,
( vd684 = vangle(sK2,sK3,sK1)
| ~ ron(sK2,vd1297)
| ~ rpoint(sK2)
| spl54_833 ),
inference(forward_subsumption_resolution,[],[f30916,f755]) ).
fof(f30974,plain,
( vd684 = vangle(sK2,sK3,sK1)
| ~ rpoint(sK2)
| spl54_833
| ~ spl54_927 ),
inference(forward_subsumption_resolution,[],[f30960,f26515]) ).
fof(f30980,plain,
( vd684 = vangle(sK2,sK3,sK1)
| spl54_833
| ~ spl54_927 ),
inference(forward_subsumption_resolution,[],[f30974,f456]) ).
fof(f30986,plain,
( vd684 = vangle(sK1,sK3,sK2)
| spl54_833
| ~ spl54_927 ),
inference(forward_demodulation,[],[f30980,f3157]) ).
fof(f33744,plain,
! [X0,X1] :
( sK2 = X0
| X0 = X1
| sK3 = X0
| ~ rpoint(X0)
| rR(X0,sK3,sK2)
| ~ rpoint(X1)
| vangle(X1,X0,sK2) = vangle(X1,X0,sK3)
| ~ rpoint(sK3) ),
inference(resolution,[],[f27836,f766]) ).
fof(f33750,plain,
! [X0,X1] :
( ~ rpoint(X1)
| X0 = X1
| sK3 = X0
| ~ rpoint(X0)
| rR(X0,sK3,sK2)
| sK2 = X0
| vangle(X1,X0,sK2) = vangle(X1,X0,sK3) ),
inference(forward_subsumption_resolution,[],[f33744,f454]) ).
fof(f33773,plain,
! [X0] :
( sK2 = X0
| sK3 = X0
| ~ rpoint(X0)
| rR(X0,sK3,sK2)
| sK2 = X0
| vangle(sK2,X0,sK2) = vangle(sK2,X0,sK3) ),
inference(resolution,[],[f33750,f456]) ).
fof(f33776,plain,
! [X0] :
( rR(X0,sK3,sK2)
| sK3 = X0
| ~ rpoint(X0)
| sK2 = X0
| vangle(sK2,X0,sK2) = vangle(sK2,X0,sK3) ),
inference(duplicate_literal_removal,[],[f33773]) ).
fof(f34235,plain,
( sK1 = sK3
| ~ rpoint(sK1)
| sK1 = sK2
| vangle(sK2,sK1,sK2) = vangle(sK2,sK1,sK3)
| spl54_935 ),
inference(resolution,[],[f33776,f27048]) ).
fof(f34250,plain,
( ~ rpoint(sK1)
| sK1 = sK2
| vangle(sK2,sK1,sK2) = vangle(sK2,sK1,sK3)
| spl54_935 ),
inference(forward_subsumption_resolution,[],[f34235,f751]) ).
fof(f34261,plain,
( sK1 = sK2
| vangle(sK2,sK1,sK2) = vangle(sK2,sK1,sK3)
| spl54_935 ),
inference(forward_subsumption_resolution,[],[f34250,f458]) ).
fof(f34271,plain,
( vangle(sK2,sK1,sK2) = vangle(sK2,sK1,sK3)
| spl54_935 ),
inference(forward_subsumption_resolution,[],[f34261,f744]) ).
fof(f34273,plain,
( vangle(sK2,sK1,sK2) = vangle(sK3,sK1,sK2)
| spl54_935 ),
inference(forward_demodulation,[],[f34271,f3144]) ).
fof(f36107,plain,
! [X0,X1] :
( rR(sK3,X0,X1)
| sK3 = X1
| sK2 = sK3
| sK3 = X0
| ~ ron(sK2,vd1295)
| vangle(sK2,sK3,X0) = vangle(sK2,sK3,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2)
| X0 = X1
| rR(sK2,vd1300,sK2)
| ~ rpoint(sK2) ),
inference(resolution,[],[f28468,f1764]) ).
fof(f36186,plain,
! [X0,X1] :
( rR(sK3,X0,X1)
| sK3 = X1
| sK2 = sK3
| sK3 = X0
| ~ ron(sK2,vd1295)
| vangle(sK2,sK3,X0) = vangle(sK2,sK3,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2)
| X0 = X1
| rR(sK2,vd1300,sK2) ),
inference(duplicate_literal_removal,[],[f36107]) ).
fof(f36224,plain,
! [X0,X1] :
( rR(sK3,X0,X1)
| sK3 = X1
| sK3 = X0
| ~ ron(sK2,vd1295)
| vangle(sK2,sK3,X0) = vangle(sK2,sK3,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2)
| X0 = X1
| rR(sK2,vd1300,sK2) ),
inference(forward_subsumption_resolution,[],[f36186,f755]) ).
fof(f36266,plain,
! [X0,X1] :
( rR(sK3,X0,X1)
| sK3 = X1
| sK3 = X0
| vangle(sK2,sK3,X0) = vangle(sK2,sK3,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2)
| X0 = X1
| rR(sK2,vd1300,sK2) ),
inference(forward_subsumption_resolution,[],[f36224,f763]) ).
fof(f36299,plain,
! [X0,X1] :
( rR(sK3,X0,X1)
| sK3 = X1
| sK3 = X0
| vangle(sK2,sK3,X0) = vangle(sK2,sK3,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X1
| rR(sK2,vd1300,sK2) ),
inference(forward_subsumption_resolution,[],[f36266,f456]) ).
fof(f36340,definition,
( spl54_982
<=> ! [X0,X1] :
( rR(sK3,X0,X1)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| vangle(sK2,sK3,X0) = vangle(sK2,sK3,X1)
| sK3 = X0
| sK3 = X1 ) ),
introduced(definition,[new_symbols(definition,[spl54_982])],[avatar_definition]) ).
fof(f36341,plain,
( ! [X0,X1] :
( rR(sK3,X0,X1)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| vangle(sK2,sK3,X0) = vangle(sK2,sK3,X1)
| sK3 = X0
| sK3 = X1 )
| ~ spl54_982 ),
inference(avatar_component_clause,[],[f36340]) ).
fof(f36650,plain,
( sK1 = sK2
| ~ rpoint(sK1)
| ~ rpoint(sK2)
| vangle(sK2,sK3,sK1) = vangle(sK2,sK3,sK2)
| sK1 = sK3
| sK2 = sK3
| spl54_805
| ~ spl54_982 ),
inference(resolution,[],[f36341,f24079]) ).
fof(f36707,plain,
( ~ rpoint(sK1)
| ~ rpoint(sK2)
| vangle(sK2,sK3,sK1) = vangle(sK2,sK3,sK2)
| sK1 = sK3
| sK2 = sK3
| spl54_805
| ~ spl54_982 ),
inference(forward_subsumption_resolution,[],[f36650,f744]) ).
fof(f36723,plain,
( ~ rpoint(sK2)
| vangle(sK2,sK3,sK1) = vangle(sK2,sK3,sK2)
| sK1 = sK3
| sK2 = sK3
| spl54_805
| ~ spl54_982 ),
inference(forward_subsumption_resolution,[],[f36707,f458]) ).
fof(f36739,plain,
( vangle(sK2,sK3,sK1) = vangle(sK2,sK3,sK2)
| sK1 = sK3
| sK2 = sK3
| spl54_805
| ~ spl54_982 ),
inference(forward_subsumption_resolution,[],[f36723,f456]) ).
fof(f36755,plain,
( vangle(sK2,sK3,sK1) = vangle(sK2,sK3,sK2)
| sK2 = sK3
| spl54_805
| ~ spl54_982 ),
inference(forward_subsumption_resolution,[],[f36739,f751]) ).
fof(f36770,plain,
( vangle(sK2,sK3,sK1) = vangle(sK2,sK3,sK2)
| spl54_805
| ~ spl54_982 ),
inference(forward_subsumption_resolution,[],[f36755,f755]) ).
fof(f36784,plain,
( vd684 = vangle(sK2,sK3,sK1)
| spl54_805
| ~ spl54_982 ),
inference(forward_demodulation,[],[f36770,f2074]) ).
fof(f36797,plain,
( vd684 = vangle(sK1,sK3,sK2)
| spl54_805
| ~ spl54_982 ),
inference(forward_demodulation,[],[f36784,f3157]) ).
fof(f39196,plain,
! [X0,X1] :
( ~ rpoint(sK1)
| ~ rpoint(sK3)
| sK2 = X0
| ~ ron(X0,sK13(sK3,sK1))
| sK1 = sK3
| rR(sK3,sK2,X0)
| ~ ron(X0,X1)
| ~ ron(sK2,X1)
| ~ ron(sK3,X1)
| ~ rline(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2) ),
inference(resolution,[],[f10313,f6151]) ).
fof(f39210,plain,
! [X0,X1] :
( ~ rpoint(sK3)
| sK2 = X0
| ~ ron(X0,sK13(sK3,sK1))
| sK1 = sK3
| rR(sK3,sK2,X0)
| ~ ron(X0,X1)
| ~ ron(sK2,X1)
| ~ ron(sK3,X1)
| ~ rline(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f39196,f458]) ).
fof(f39219,plain,
! [X0,X1] :
( sK2 = X0
| ~ ron(X0,sK13(sK3,sK1))
| sK1 = sK3
| rR(sK3,sK2,X0)
| ~ ron(X0,X1)
| ~ ron(sK2,X1)
| ~ ron(sK3,X1)
| ~ rline(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f39210,f454]) ).
fof(f39228,plain,
! [X0,X1] :
( sK2 = X0
| ~ ron(X0,sK13(sK3,sK1))
| rR(sK3,sK2,X0)
| ~ ron(X0,X1)
| ~ ron(sK2,X1)
| ~ ron(sK3,X1)
| ~ rline(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2) ),
inference(forward_subsumption_resolution,[],[f39219,f751]) ).
fof(f39237,plain,
! [X0,X1] :
( ~ ron(X0,sK13(sK3,sK1))
| sK2 = X0
| rR(sK3,sK2,X0)
| ~ ron(X0,X1)
| ~ ron(sK2,X1)
| ~ ron(sK3,X1)
| ~ rline(X1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f39228,f456]) ).
fof(f39247,plain,
! [X0] :
( sK1 = sK2
| rR(sK3,sK2,sK1)
| ~ ron(sK1,X0)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK1) ),
inference(resolution,[],[f39237,f6163]) ).
fof(f39301,plain,
( ~ rline(vd1297)
| ~ ron(sK1,vd1297)
| ~ spl54_804 ),
inference(resolution,[],[f24075,f764]) ).
fof(f39310,plain,
( ~ ron(sK1,vd1297)
| ~ spl54_804 ),
inference(forward_subsumption_resolution,[],[f39301,f498]) ).
fof(f39315,plain,
( $false
| ~ spl54_804 ),
inference(forward_subsumption_resolution,[],[f39310,f762]) ).
fof(f39316,plain,
~ spl54_804,
inference(avatar_contradiction_clause,[],[f39315]) ).
fof(f39730,plain,
! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ~ rR(sK3,sK2,sK1)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| sK2 = sK3
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f3265,f751]) ).
fof(f39796,definition,
( spl54_1011
<=> vd684 = vangle(sK1,sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl54_1011])],[avatar_definition]) ).
fof(f39797,plain,
( vd684 = vangle(sK1,sK3,sK2)
| ~ spl54_1011 ),
inference(avatar_component_clause,[],[f39796]) ).
fof(f39944,definition,
( spl54_1023
<=> rR(sK2,vd1300,sK2) ),
introduced(definition,[new_symbols(definition,[spl54_1023])],[avatar_definition]) ).
fof(f39946,plain,
( rR(sK2,vd1300,sK2)
| ~ spl54_1023 ),
inference(avatar_component_clause,[],[f39944]) ).
fof(f39998,plain,
( spl54_1011
| spl54_833
| ~ spl54_927 ),
inference(avatar_split_clause,[],[f30986,f26514,f24399,f39796]) ).
fof(f40238,plain,
( spl54_1011
| spl54_805
| ~ spl54_982 ),
inference(avatar_split_clause,[],[f36797,f36340,f24077,f39796]) ).
fof(f40288,plain,
! [X0] :
( rR(sK3,sK2,sK1)
| ~ ron(sK1,X0)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f39247,f744]) ).
fof(f40605,plain,
! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ~ rR(sK3,sK2,sK1)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f39730,f755]) ).
fof(f40847,plain,
! [X0] :
( rR(sK3,sK2,sK1)
| ~ ron(sK1,X0)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f40288,f458]) ).
fof(f40850,definition,
( spl54_1069
<=> rR(sK3,sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl54_1069])],[avatar_definition]) ).
fof(f40851,plain,
( ~ rR(sK3,sK2,sK1)
| spl54_1069 ),
inference(avatar_component_clause,[],[f40850]) ).
fof(f40854,definition,
( spl54_1070
<=> ! [X0] :
( ~ ron(sK1,X0)
| ~ rline(X0)
| ~ ron(sK3,X0)
| ~ ron(sK2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_1070])],[avatar_definition]) ).
fof(f40855,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ rline(X0)
| ~ ron(sK3,X0)
| ~ ron(sK2,X0) )
| ~ spl54_1070 ),
inference(avatar_component_clause,[],[f40854]) ).
fof(f41074,plain,
! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ~ rR(sK3,sK2,sK1)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f40605,f458]) ).
fof(f41453,plain,
! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ~ rR(sK3,sK2,sK1)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f41074,f456]) ).
fof(f41751,plain,
! [X0] :
( vd684 != vangle(sK1,sK3,sK2)
| ~ rR(sK3,sK2,sK1)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f41453,f454]) ).
fof(f42002,plain,
( spl54_832
| ~ spl54_1069
| ~ spl54_1011 ),
inference(avatar_split_clause,[],[f41751,f39796,f40850,f24396]) ).
fof(f42880,plain,
( ~ ron(sK2,vd1295)
| sK1 = sK2
| ~ rpoint(sK2)
| spl54_931
| spl54_935 ),
inference(forward_subsumption_resolution,[],[f30331,f26618]) ).
fof(f42881,plain,
( vd684 = vangle(sK3,sK1,sK2)
| spl54_935 ),
inference(forward_demodulation,[],[f34273,f2152]) ).
fof(f43436,plain,
( sK1 = sK2
| ~ rpoint(sK2)
| spl54_931
| spl54_935 ),
inference(forward_subsumption_resolution,[],[f42880,f763]) ).
fof(f43437,plain,
( $false
| spl54_931
| spl54_935 ),
inference(forward_subsumption_resolution,[],[f42881,f26618]) ).
fof(f43438,plain,
( spl54_931
| spl54_935 ),
inference(avatar_contradiction_clause,[],[f43437]) ).
fof(f43890,plain,
( ~ rpoint(sK2)
| spl54_931
| spl54_935 ),
inference(forward_subsumption_resolution,[],[f43436,f744]) ).
fof(f44220,plain,
( $false
| spl54_931
| spl54_935 ),
inference(forward_subsumption_resolution,[],[f43890,f456]) ).
fof(f44221,plain,
( spl54_931
| spl54_935 ),
inference(avatar_contradiction_clause,[],[f44220]) ).
fof(f47277,plain,
( ~ rR(sK3,sK1,sK2)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ spl54_935 ),
inference(resolution,[],[f27047,f789]) ).
fof(f47280,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ron(sK2,X0)
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_935 ),
inference(resolution,[],[f27047,f902]) ).
fof(f47289,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_832
| ~ spl54_935 ),
inference(forward_subsumption_resolution,[],[f47280,f24397]) ).
fof(f47292,plain,
( ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ spl54_805
| ~ spl54_935 ),
inference(forward_subsumption_resolution,[],[f47277,f24078]) ).
fof(f47298,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_832
| ~ spl54_935 ),
inference(forward_subsumption_resolution,[],[f47289,f456]) ).
fof(f47300,plain,
( ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ spl54_805
| ~ spl54_935 ),
inference(forward_subsumption_resolution,[],[f47292,f456]) ).
fof(f47306,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK3) )
| ~ spl54_832
| ~ spl54_935 ),
inference(forward_subsumption_resolution,[],[f47298,f458]) ).
fof(f47308,plain,
( ~ rpoint(sK1)
| ~ spl54_805
| ~ spl54_935 ),
inference(forward_subsumption_resolution,[],[f47300,f454]) ).
fof(f47311,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) )
| ~ spl54_832
| ~ spl54_935 ),
inference(forward_subsumption_resolution,[],[f47306,f454]) ).
fof(f47313,plain,
( $false
| ~ spl54_805
| ~ spl54_935 ),
inference(forward_subsumption_resolution,[],[f47308,f458]) ).
fof(f47314,plain,
( ~ spl54_805
| ~ spl54_935 ),
inference(avatar_contradiction_clause,[],[f47313]) ).
fof(f47316,plain,
( spl54_804
| ~ spl54_832
| ~ spl54_935 ),
inference(avatar_split_clause,[],[f47311,f27046,f24396,f24074]) ).
fof(f47444,plain,
( ! [X0] :
( vd684 != vangle(sK3,sK1,sK2)
| ~ ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK1) )
| ~ spl54_832 ),
inference(forward_subsumption_resolution,[],[f23673,f24397]) ).
fof(f47449,plain,
( ! [X0] :
( ~ ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK1) )
| ~ spl54_832
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f47444,f26619]) ).
fof(f47453,plain,
( ! [X0] :
( ~ ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ rline(X0) )
| ~ spl54_832
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f47449,f458]) ).
fof(f47457,plain,
( spl54_818
| ~ spl54_832
| ~ spl54_931 ),
inference(avatar_split_clause,[],[f47453,f26617,f24396,f24241]) ).
fof(f47476,plain,
( ! [X0] :
( vd684 != vd684
| ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| sK2 = sK3
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1011 ),
inference(superposition,[],[f951,f39797]) ).
fof(f47477,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| sK2 = sK3
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1011 ),
inference(trivial_inequality_removal,[],[f47476]) ).
fof(f47479,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1011 ),
inference(forward_subsumption_resolution,[],[f47477,f755]) ).
fof(f47488,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1011 ),
inference(forward_subsumption_resolution,[],[f47479,f751]) ).
fof(f47497,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK3) )
| ~ spl54_1011 ),
inference(forward_subsumption_resolution,[],[f47488,f456]) ).
fof(f47506,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| ~ rpoint(sK3) )
| ~ spl54_1011 ),
inference(forward_subsumption_resolution,[],[f47497,f458]) ).
fof(f47515,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) )
| ~ spl54_1011 ),
inference(forward_subsumption_resolution,[],[f47506,f454]) ).
fof(f47524,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) )
| ~ spl54_818
| ~ spl54_1011 ),
inference(forward_subsumption_resolution,[],[f47515,f24242]) ).
fof(f47533,plain,
( spl54_804
| ~ spl54_818
| ~ spl54_1011 ),
inference(avatar_split_clause,[],[f47524,f39796,f24241,f24074]) ).
fof(f47588,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) )
| spl54_1069 ),
inference(forward_subsumption_resolution,[],[f40847,f40851]) ).
fof(f47603,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ rline(X0) )
| ~ spl54_1011
| ~ spl54_1070 ),
inference(forward_subsumption_resolution,[],[f47515,f40855]) ).
fof(f47611,plain,
( spl54_804
| ~ spl54_1011
| ~ spl54_1070 ),
inference(avatar_split_clause,[],[f47603,f40854,f39796,f24074]) ).
fof(f47734,plain,
( spl54_1070
| spl54_1069 ),
inference(avatar_split_clause,[],[f47588,f40850,f40854]) ).
fof(f47757,plain,
( spl54_1023
| spl54_982 ),
inference(avatar_split_clause,[],[f36299,f36340,f39944]) ).
fof(f49065,plain,
( ! [X0] :
( vd684 != vd684
| ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| sK1 = sK2
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_931 ),
inference(superposition,[],[f951,f26619]) ).
fof(f49066,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| sK1 = sK2
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_931 ),
inference(trivial_inequality_removal,[],[f49065]) ).
fof(f49068,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f49066,f744]) ).
fof(f49077,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f49068,f751]) ).
fof(f49086,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f49077,f456]) ).
fof(f49095,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK1) )
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f49086,f454]) ).
fof(f49104,plain,
( ! [X0] :
( ~ ron(sK3,X0)
| ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ rline(X0) )
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f49095,f458]) ).
fof(f49187,plain,
( ron(sK2,vd1297)
| ~ ron(sK1,vd1297)
| ~ rline(vd1297)
| ~ spl54_931 ),
inference(resolution,[],[f49104,f764]) ).
fof(f49195,plain,
( ~ ron(sK1,vd1297)
| ~ rline(vd1297)
| spl54_927
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f49187,f26516]) ).
fof(f49198,plain,
( ~ rline(vd1297)
| spl54_927
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f49195,f762]) ).
fof(f49199,plain,
( $false
| spl54_927
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f49198,f498]) ).
fof(f49200,plain,
( spl54_927
| ~ spl54_931 ),
inference(avatar_contradiction_clause,[],[f49199]) ).
fof(f49595,plain,
( vf(sK2,vd1306) = vplus(vf(sK2,sK3),vf(sK3,vd1306))
| ~ rpoint(vd1306)
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ spl54_833 ),
inference(resolution,[],[f24400,f1054]) ).
fof(f49599,plain,
( vf(sK2,vd1306) = vplus(vf(sK2,sK3),vf(sK3,vd1306))
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ spl54_833 ),
inference(forward_subsumption_resolution,[],[f49595,f449]) ).
fof(f49604,plain,
( vf(sK2,vd1306) = vplus(vf(sK2,sK3),vf(sK3,vd1306))
| ~ rpoint(sK2)
| ~ spl54_833 ),
inference(forward_subsumption_resolution,[],[f49599,f454]) ).
fof(f49609,plain,
( vf(sK2,vd1306) = vplus(vf(sK2,sK3),vf(sK3,vd1306))
| ~ spl54_833 ),
inference(forward_subsumption_resolution,[],[f49604,f456]) ).
fof(f49613,plain,
( vf(sK2,vd1306) = vplus(vf(sK2,sK3),vf(sK3,vd1300))
| ~ spl54_833 ),
inference(forward_demodulation,[],[f49609,f750]) ).
fof(f49615,plain,
( vf(sK2,vd1306) = vplus(vf(sK2,sK3),sK7(sK3,vd1300))
| ~ spl54_833 ),
inference(forward_demodulation,[],[f49613,f5678]) ).
fof(f50093,plain,
( ! [X0] :
( ~ rR(sK2,sK3,X0)
| rR(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_805 ),
inference(resolution,[],[f24078,f786]) ).
fof(f50106,plain,
( ! [X0] :
( ~ rR(sK2,sK3,X0)
| rR(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_805 ),
inference(forward_subsumption_resolution,[],[f50093,f456]) ).
fof(f50111,plain,
( ! [X0] :
( ~ rR(sK2,sK3,X0)
| rR(sK3,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK1) )
| ~ spl54_805 ),
inference(forward_subsumption_resolution,[],[f50106,f454]) ).
fof(f50116,plain,
( ! [X0] :
( ~ rR(sK2,sK3,X0)
| rR(sK3,sK1,X0)
| ~ rpoint(X0) )
| ~ spl54_805 ),
inference(forward_subsumption_resolution,[],[f50111,f458]) ).
fof(f50535,plain,
( rR(sK2,sK2,vd1300)
| ~ rpoint(sK2)
| ~ rpoint(sK2)
| ~ rpoint(vd1300)
| ~ spl54_1023 ),
inference(resolution,[],[f39946,f800]) ).
fof(f50548,plain,
( rR(sK2,sK2,vd1300)
| ~ rpoint(sK2)
| ~ rpoint(vd1300)
| ~ spl54_1023 ),
inference(duplicate_literal_removal,[],[f50535]) ).
fof(f50553,plain,
( ~ rpoint(sK2)
| ~ rpoint(vd1300)
| ~ spl54_1023 ),
inference(forward_subsumption_resolution,[],[f50548,f1552]) ).
fof(f50556,plain,
( ~ rpoint(vd1300)
| ~ spl54_1023 ),
inference(forward_subsumption_resolution,[],[f50553,f456]) ).
fof(f50559,plain,
( $false
| ~ spl54_1023 ),
inference(forward_subsumption_resolution,[],[f50556,f472]) ).
fof(f50560,plain,
~ spl54_1023,
inference(avatar_contradiction_clause,[],[f50559]) ).
fof(f54234,plain,
( vf(sK2,vd1306) = vplus(vf(sK3,sK1),sK7(sK3,vd1300))
| ~ spl54_833 ),
inference(forward_demodulation,[],[f49615,f1783]) ).
fof(f54523,plain,
( vf(sK2,vd1306) = vplus(sK7(sK2,sK3),sK7(sK3,vd1300))
| ~ spl54_833 ),
inference(forward_demodulation,[],[f54234,f5653]) ).
fof(f55756,plain,
( rR(sK3,sK1,vd1300)
| ~ rpoint(vd1300)
| ~ spl54_805 ),
inference(resolution,[],[f50116,f742]) ).
fof(f55816,plain,
( rR(sK3,sK1,vd1300)
| ~ spl54_805 ),
inference(forward_subsumption_resolution,[],[f55756,f472]) ).
fof(f55863,plain,
( vf(sK1,vd1300) = vplus(vf(sK1,sK3),vf(sK3,vd1300))
| ~ rpoint(vd1300)
| ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ spl54_805 ),
inference(resolution,[],[f55816,f1054]) ).
fof(f55868,plain,
( vf(sK1,vd1300) = vplus(vf(sK1,sK3),vf(sK3,vd1300))
| ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ spl54_805 ),
inference(forward_subsumption_resolution,[],[f55863,f472]) ).
fof(f55876,plain,
( vf(sK1,vd1300) = vplus(vf(sK1,sK3),vf(sK3,vd1300))
| ~ rpoint(sK1)
| ~ spl54_805 ),
inference(forward_subsumption_resolution,[],[f55868,f454]) ).
fof(f55883,plain,
( vf(sK1,vd1300) = vplus(vf(sK1,sK3),vf(sK3,vd1300))
| ~ spl54_805 ),
inference(forward_subsumption_resolution,[],[f55876,f458]) ).
fof(f55888,plain,
( vf(sK1,vd1300) = vplus(vf(sK1,sK3),sK7(sK3,vd1300))
| ~ spl54_805 ),
inference(forward_demodulation,[],[f55883,f5678]) ).
fof(f56512,plain,
( vf(sK2,vd1306) = vplus(sK7(sK3,sK1),sK7(sK3,vd1300))
| ~ spl54_833 ),
inference(forward_demodulation,[],[f54523,f5690]) ).
fof(f56520,plain,
( vf(sK1,vd1300) = vplus(vf(sK3,sK1),sK7(sK3,vd1300))
| ~ spl54_805 ),
inference(forward_demodulation,[],[f55888,f1789]) ).
fof(f56664,plain,
( sF53 = vplus(sK7(sK3,sK1),sK7(sK3,vd1300))
| ~ spl54_833 ),
inference(forward_demodulation,[],[f56512,f1678]) ).
fof(f56669,plain,
( vf(sK1,vd1300) = vplus(sK7(sK2,sK3),sK7(sK3,vd1300))
| ~ spl54_805 ),
inference(forward_demodulation,[],[f56520,f5653]) ).
fof(f56771,plain,
( vf(sK1,vd1300) = vplus(sK7(sK3,sK1),sK7(sK3,vd1300))
| ~ spl54_805 ),
inference(forward_demodulation,[],[f56669,f5690]) ).
fof(f56845,plain,
( sF53 = vf(sK1,vd1300)
| ~ spl54_805
| ~ spl54_833 ),
inference(forward_demodulation,[],[f56771,f56664]) ).
fof(f56965,plain,
( sF52 = sF53
| ~ spl54_805
| ~ spl54_833 ),
inference(forward_demodulation,[],[f56845,f1668]) ).
fof(f56978,plain,
( $false
| ~ spl54_805
| ~ spl54_833 ),
inference(forward_subsumption_resolution,[],[f56965,f1550]) ).
fof(f56979,plain,
( ~ spl54_805
| ~ spl54_833 ),
inference(avatar_contradiction_clause,[],[f56978]) ).
cnf(s1166,plain,
~ spl54_804,
inference(sat_conversion,[],[f39316]) ).
cnf(s1206,plain,
( spl54_833
| ~ spl54_927
| spl54_1011 ),
inference(sat_conversion,[],[f39998]) ).
cnf(s1248,plain,
( spl54_805
| ~ spl54_982
| spl54_1011 ),
inference(sat_conversion,[],[f40238]) ).
cnf(s1356,plain,
( spl54_832
| ~ spl54_1011
| ~ spl54_1069 ),
inference(sat_conversion,[],[f42002]) ).
cnf(s1457,plain,
( spl54_931
| spl54_935 ),
inference(sat_conversion,[],[f43438]) ).
cnf(s1478,plain,
( spl54_931
| spl54_935 ),
inference(sat_conversion,[],[f44221]) ).
cnf(s1753,plain,
( ~ spl54_805
| ~ spl54_935 ),
inference(sat_conversion,[],[f47314]) ).
cnf(s1754,plain,
( spl54_804
| ~ spl54_832
| ~ spl54_935 ),
inference(sat_conversion,[],[f47316]) ).
cnf(s1765,plain,
( spl54_818
| ~ spl54_832
| ~ spl54_931 ),
inference(sat_conversion,[],[f47457]) ).
cnf(s1766,plain,
( spl54_804
| ~ spl54_818
| ~ spl54_1011 ),
inference(sat_conversion,[],[f47533]) ).
cnf(s1774,plain,
( spl54_804
| ~ spl54_1011
| ~ spl54_1070 ),
inference(sat_conversion,[],[f47611]) ).
cnf(s1782,plain,
( spl54_1069
| spl54_1070 ),
inference(sat_conversion,[],[f47734]) ).
cnf(s1790,plain,
( spl54_982
| spl54_1023 ),
inference(sat_conversion,[],[f47757]) ).
cnf(s1917,plain,
( spl54_927
| ~ spl54_931 ),
inference(sat_conversion,[],[f49200]) ).
cnf(s1955,plain,
~ spl54_1023,
inference(sat_conversion,[],[f50560]) ).
cnf(s2162,plain,
( ~ spl54_805
| ~ spl54_833 ),
inference(sat_conversion,[],[f56979]) ).
cnf(s2164,plain,
spl54_982,
inference(rat,[],[s1790,s1955]) ).
cnf(s2186,plain,
( spl54_805
| spl54_1011 ),
inference(rat,[],[s1248,s2164]) ).
cnf(s2368,plain,
( ~ spl54_832
| spl54_818 ),
inference(rat,[],[s1457,s1754,s1765,s1166]) ).
cnf(s2369,plain,
~ spl54_1011,
inference(rat,[],[s2368,s1356,s1782,s1766,s1774,s1166]) ).
cnf(s2370,plain,
spl54_805,
inference(rat,[],[s2186,s2369]) ).
cnf(s2371,plain,
~ spl54_833,
inference(rat,[],[s2162,s2370]) ).
cnf(s2378,plain,
~ spl54_935,
inference(rat,[],[s1753,s2370]) ).
cnf(s2381,plain,
~ spl54_927,
inference(rat,[],[s1206,s2369,s2371]) ).
cnf(s2394,plain,
spl54_931,
inference(rat,[],[s1478,s2378]) ).
cnf(s2400,plain,
$false,
inference(rat,[],[s1917,s2394,s2381]) ).
fof(f56980,plain,
$false,
inference(avatar_sat_refutation,[],[s2400]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO309+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n009.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 08:03:15 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.69/2.79 % (1707208)Detected formulas, will run a generic FOF schedule.
% 12.69/2.79 % (1707213)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=1158174729:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.69/2.79 % (1707217)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2435865536:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.69/2.79 % (1707216)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1197663239:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.69/2.79 % (1707214)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=150357966:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.69/2.79 % (1707215)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=1167780206:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.69/2.79 % (1707218)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3719758621:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.69/2.79 % (1707216)Refutation not found, incomplete strategy
% 12.69/2.79 % (1707216)------------------------------
% 12.69/2.79 % (1707216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.69/2.79 % (1707216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.69/2.79 % (1707216)CaDiCaL version: 2.1.3
% 12.69/2.79 % (1707216)Termination reason: Refutation not found, incomplete strategy
% 12.69/2.79 % (1707216)Time elapsed: 0.003 s
% 12.69/2.79 % (1707216)Peak memory usage: 89 MB
% 12.69/2.79 % (1707216)Instructions burned: 2 (million)
% 12.69/2.79 % (1707219)dis-21_1_sil=8000:lcm=predicate:random_seed=935676184:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 12.69/2.79 % (1707217)Instruction limit reached!
% 12.69/2.79 % (1707217)------------------------------
% 12.69/2.79 % (1707217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.69/2.79 % (1707217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.69/2.79 % (1707217)CaDiCaL version: 2.1.3
% 12.69/2.79 % (1707217)Termination reason: Instruction limit
% 12.69/2.79 % (1707217)Termination phase: Saturation
% 12.69/2.79 % (1707217)Time elapsed: 0.064 s
% 12.69/2.79 % (1707217)Peak memory usage: 88 MB
% 12.69/2.79 % (1707217)Instructions burned: 120 (million)
% 12.69/2.79 % (1707219)Instruction limit reached!
% 12.69/2.79 % (1707219)------------------------------
% 12.69/2.79 % (1707219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.69/2.79 % (1707219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.69/2.79 % (1707219)CaDiCaL version: 2.1.3
% 12.69/2.79 % (1707219)Termination reason: Instruction limit
% 12.69/2.79 % (1707219)Termination phase: Saturation
% 12.69/2.79 % (1707219)Time elapsed: 0.069 s
% 12.69/2.79 % (1707219)Peak memory usage: 90 MB
% 12.69/2.79 % (1707219)Instructions burned: 129 (million)
% 12.69/2.79 % (1707218)Instruction limit reached!
% 12.69/2.79 % (1707218)------------------------------
% 12.69/2.79 % (1707218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.69/2.79 % (1707218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.69/2.79 % (1707218)CaDiCaL version: 2.1.3
% 12.69/2.79 % (1707218)Termination reason: Instruction limit
% 12.69/2.79 % (1707218)Termination phase: Saturation
% 12.69/2.79 % (1707218)Time elapsed: 0.084 s
% 12.69/2.79 % (1707218)Peak memory usage: 90 MB
% 12.69/2.79 % (1707218)Instructions burned: 140 (million)
% 12.69/2.79 % (1707227)lrs+10_1_sil=8000:sp=occurrence:random_seed=262164062:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.69/2.79 % (1707228)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3776885198:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.69/2.79 % (1707228)Refutation not found, incomplete strategy
% 12.69/2.79 % (1707228)------------------------------
% 12.69/2.79 % (1707228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.69/2.79 % (1707228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.69/2.79 % (1707228)CaDiCaL version: 2.1.3
% 12.69/2.79 % (1707228)Termination reason: Refutation not found, incomplete strategy
% 20.21/3.76 % (1707228)Time elapsed: 0.004 s
% 20.21/3.76 % (1707228)Peak memory usage: 89 MB
% 20.21/3.76 % (1707228)Instructions burned: 4 (million)
% 20.21/3.76 % (1707229)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2945808538:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 20.21/3.76 % (1707216)------------------------------
% 20.21/3.76 % (1707216)------------------------------
% 20.21/3.76 % (1707227)Instruction limit reached!
% 20.21/3.76 % (1707227)------------------------------
% 20.21/3.76 % (1707227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.21/3.76 % (1707227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.21/3.76 % (1707227)CaDiCaL version: 2.1.3
% 20.21/3.76 % (1707227)Termination reason: Instruction limit
% 20.21/3.76 % (1707227)Termination phase: Saturation
% 20.21/3.76 % (1707227)Time elapsed: 0.142 s
% 20.21/3.76 % (1707227)Peak memory usage: 91 MB
% 20.21/3.76 % (1707227)Instructions burned: 285 (million)
% 20.21/3.76 % (1707233)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=1866836874:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 20.21/3.76 % (1707229)Instruction limit reached!
% 20.21/3.76 % (1707229)------------------------------
% 20.21/3.76 % (1707229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.21/3.76 % (1707229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.21/3.76 % (1707229)CaDiCaL version: 2.1.3
% 20.21/3.76 % (1707229)Termination reason: Instruction limit
% 20.21/3.76 % (1707229)Termination phase: Saturation
% 20.21/3.76 % (1707229)Time elapsed: 0.164 s
% 20.21/3.76 % (1707229)Peak memory usage: 90 MB
% 20.21/3.76 % (1707229)Instructions burned: 325 (million)
% 20.21/3.76 % (1707228)------------------------------
% 20.21/3.76 % (1707228)------------------------------
% 20.21/3.76 % (1707234)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3158825952:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 20.21/3.76 % (1707233)Instruction limit reached!
% 20.21/3.76 % (1707233)------------------------------
% 20.21/3.76 % (1707233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.21/3.76 % (1707233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.21/3.76 % (1707233)CaDiCaL version: 2.1.3
% 20.21/3.76 % (1707233)Termination reason: Instruction limit
% 20.21/3.76 % (1707233)Termination phase: Saturation
% 20.21/3.76 % (1707233)Time elapsed: 0.118 s
% 20.21/3.76 % (1707233)Peak memory usage: 93 MB
% 20.21/3.76 % (1707233)Instructions burned: 250 (million)
% 20.21/3.76 % (1707236)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1076741169:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 20.21/3.76 % (1707237)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1496340281:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 20.21/3.76 % (1707234)Instruction limit reached!
% 20.21/3.76 % (1707234)------------------------------
% 20.21/3.76 % (1707234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.21/3.76 % (1707234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.21/3.76 % (1707234)CaDiCaL version: 2.1.3
% 20.21/3.76 % (1707234)Termination reason: Instruction limit
% 20.21/3.76 % (1707234)Termination phase: Saturation
% 20.21/3.76 % (1707234)Time elapsed: 0.141 s
% 20.21/3.76 % (1707234)Peak memory usage: 90 MB
% 20.21/3.76 % (1707234)Instructions burned: 296 (million)
% 20.21/3.76 % (1707239)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2949408652:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 20.21/3.76 % (1707237)Instruction limit reached!
% 20.21/3.76 % (1707237)------------------------------
% 20.21/3.76 % (1707237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.21/3.76 % (1707237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.21/3.76 % (1707237)CaDiCaL version: 2.1.3
% 20.21/3.76 % (1707237)Termination reason: Instruction limit
% 20.21/3.76 % (1707237)Termination phase: Saturation
% 20.21/3.76 % (1707237)Time elapsed: 0.057 s
% 20.21/3.76 % (1707237)Peak memory usage: 89 MB
% 20.21/3.76 % (1707237)Instructions burned: 113 (million)
% 20.21/3.76 % (1707239)Refutation not found, incomplete strategy
% 20.21/3.76 % (1707239)------------------------------
% 20.21/3.76 % (1707239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.21/3.76 % (1707239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/4.14 % (1707239)CaDiCaL version: 2.1.3
% 19.70/4.14 % (1707239)Termination reason: Refutation not found, incomplete strategy
% 19.70/4.14 % (1707239)Time elapsed: 0.025 s
% 19.70/4.14 % (1707239)Peak memory usage: 89 MB
% 19.70/4.14 % (1707239)Instructions burned: 53 (million)
% 19.70/4.14 % (1707242)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1473153547:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 19.70/4.14 % (1707244)lrs+10_1_sil=8000:sp=occurrence:random_seed=2137674764:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 19.70/4.14 % (1707242)Instruction limit reached!
% 19.70/4.14 % (1707242)------------------------------
% 19.70/4.14 % (1707242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.70/4.14 % (1707242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/4.14 % (1707242)CaDiCaL version: 2.1.3
% 19.70/4.14 % (1707242)Termination reason: Instruction limit
% 19.70/4.14 % (1707242)Termination phase: Saturation
% 19.70/4.14 % (1707242)Time elapsed: 0.061 s
% 19.70/4.14 % (1707242)Peak memory usage: 89 MB
% 19.70/4.14 % (1707242)Instructions burned: 115 (million)
% 19.70/4.14 % (1707239)------------------------------
% 19.70/4.14 % (1707239)------------------------------
% 19.70/4.14 % (1707247)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3589634329:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 19.70/4.14 % (1707247)Refutation not found, incomplete strategy
% 19.70/4.14 % (1707247)------------------------------
% 19.70/4.14 % (1707247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.70/4.14 % (1707247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/4.14 % (1707247)CaDiCaL version: 2.1.3
% 19.70/4.14 % (1707247)Termination reason: Refutation not found, incomplete strategy
% 19.70/4.14 % (1707247)Time elapsed: 0.017 s
% 19.70/4.14 % (1707247)Peak memory usage: 89 MB
% 19.70/4.14 % (1707247)Instructions burned: 31 (million)
% 19.70/4.14 % (1707248)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2269695516:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 19.70/4.14 % (1707247)------------------------------
% 19.70/4.14 % (1707247)------------------------------
% 19.70/4.14 % (1707244)Instruction limit reached!
% 19.70/4.14 % (1707244)------------------------------
% 19.70/4.14 % (1707244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.70/4.14 % (1707244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/4.14 % (1707244)CaDiCaL version: 2.1.3
% 19.70/4.14 % (1707244)Termination reason: Instruction limit
% 19.70/4.14 % (1707244)Termination phase: Saturation
% 19.70/4.14 % (1707244)Time elapsed: 0.476 s
% 19.70/4.14 % (1707244)Peak memory usage: 98 MB
% 19.70/4.14 % (1707244)Instructions burned: 908 (million)
% 19.70/4.14 % (1707251)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2308259877:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 19.70/4.14 % (1707251)Instruction limit reached!
% 19.70/4.14 % (1707251)------------------------------
% 19.70/4.14 % (1707251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.70/4.14 % (1707251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/4.14 % (1707251)CaDiCaL version: 2.1.3
% 19.70/4.14 % (1707251)Termination reason: Instruction limit
% 19.70/4.14 % (1707251)Termination phase: Saturation
% 19.70/4.14 % (1707251)Time elapsed: 0.066 s
% 19.70/4.14 % (1707251)Peak memory usage: 93 MB
% 19.70/4.14 % (1707251)Instructions burned: 134 (million)
% 19.70/4.14 % (1707252)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2645011642:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 19.70/4.14 % (1707254)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1061298244:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 19.70/4.14 % (1707252)Instruction limit reached!
% 19.70/4.14 % (1707252)------------------------------
% 19.70/4.14 % (1707252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.70/4.14 % (1707252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/4.14 % (1707252)CaDiCaL version: 2.1.3
% 19.70/4.14 % (1707252)Termination reason: Instruction limit
% 19.70/4.14 % (1707252)Termination phase: Saturation
% 19.70/4.14 % (1707252)Time elapsed: 0.369 s
% 19.70/4.14 % (1707252)Peak memory usage: 97 MB
% 19.70/4.14 % (1707252)Instructions burned: 593 (million)
% 19.70/4.14 % (1707257)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=979190350:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 19.70/4.14 % (1707257)Refutation not found, incomplete strategy
% 19.70/4.14 % (1707257)------------------------------
% 19.70/4.14 % (1707257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.70/4.14 % (1707257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/4.14 % (1707257)CaDiCaL version: 2.1.3
% 19.70/4.14 % (1707257)Termination reason: Refutation not found, incomplete strategy
% 19.70/4.14 % (1707257)Time elapsed: 0.019 s
% 19.70/4.14 % (1707257)Peak memory usage: 89 MB
% 19.70/4.14 % (1707257)Instructions burned: 34 (million)
% 19.70/4.14 % (1707236)Instruction limit reached!
% 19.70/4.14 % (1707236)------------------------------
% 19.70/4.14 % (1707236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.70/4.14 % (1707236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/4.14 % (1707236)CaDiCaL version: 2.1.3
% 19.70/4.14 % (1707236)Termination reason: Instruction limit
% 19.70/4.14 % (1707236)Termination phase: Saturation
% 19.70/4.14 % (1707236)Time elapsed: 1.462 s
% 19.70/4.14 % (1707236)Peak memory usage: 141 MB
% 19.70/4.14 % (1707236)Instructions burned: 2351 (million)
% 19.70/4.14 % (1707259)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=479809276:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 19.70/4.14 % (1707257)------------------------------
% 19.70/4.14 % (1707257)------------------------------
% 19.70/4.14 % (1707259)Instruction limit reached!
% 19.70/4.14 % (1707259)------------------------------
% 19.70/4.14 % (1707259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.70/4.14 % (1707259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/4.14 % (1707259)CaDiCaL version: 2.1.3
% 19.70/4.14 % (1707259)Termination reason: Instruction limit
% 19.70/4.14 % (1707259)Termination phase: Saturation
% 19.70/4.14 % (1707259)Time elapsed: 0.077 s
% 19.70/4.14 % (1707259)Peak memory usage: 91 MB
% 19.70/4.14 % (1707259)Instructions burned: 135 (million)
% 19.70/4.14 % (1707261)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=151301498:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 19.70/4.14 % (1707261)Refutation not found, incomplete strategy
% 19.70/4.14 % (1707261)------------------------------
% 19.70/4.14 % (1707261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.70/4.14 % (1707261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/4.14 % (1707261)CaDiCaL version: 2.1.3
% 19.70/4.14 % (1707261)Termination reason: Refutation not found, incomplete strategy
% 19.70/4.14 % (1707261)Time elapsed: 0.002 s
% 19.70/4.14 % (1707261)Peak memory usage: 88 MB
% 19.70/4.14 % (1707261)Instructions burned: 1 (million)
% 19.70/4.14 % (1707262)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1518089558:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 19.70/4.14 % (1707262)Refutation not found, incomplete strategy
% 19.70/4.14 % (1707262)------------------------------
% 19.70/4.14 % (1707262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.70/4.14 % (1707262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/4.14 % (1707262)CaDiCaL version: 2.1.3
% 19.70/4.14 % (1707262)Termination reason: Refutation not found, incomplete strategy
% 19.70/4.14 % (1707262)Time elapsed: 0.006 s
% 19.70/4.14 % (1707262)Peak memory usage: 88 MB
% 19.70/4.14 % (1707262)Instructions burned: 9 (million)
% 19.70/4.14 % (1707261)------------------------------
% 19.70/4.14 % (1707261)------------------------------
% 19.70/4.14 % (1707262)------------------------------
% 19.70/4.14 % (1707262)------------------------------
% 19.70/4.14 % (1707265)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=3299133118:i=6060:aac=none:ins=25_2972 on theBenchmark for (2972ds/6060Mi)
% 19.70/4.14 % (1707266)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=2139286467:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 19.70/4.14 % (1707266)Instruction limit reached!
% 19.70/4.14 % (1707266)------------------------------
% 19.70/4.14 % (1707266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.70/4.14 % (1707266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/4.14 % (1707266)CaDiCaL version: 2.1.3
% 19.70/4.14 % (1707266)Termination reason: Instruction limit
% 19.70/4.14 % (1707266)Termination phase: Saturation
% 19.70/4.14 % (1707266)Time elapsed: 0.075 s
% 19.70/4.14 % (1707266)Peak memory usage: 92 MB
% 19.70/4.14 % (1707266)Instructions burned: 150 (million)
% 19.70/4.14 % (1707213)First to succeed.
% 19.70/4.14 % (1707269)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2534264543:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 19.70/4.14 % (1707213)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1707208"
% 19.70/4.14 % (1707213)Refutation found. Thanks to Tanya!
% 19.70/4.14 % SZS status Theorem for theBenchmark
% 19.70/4.14 % SZS output start Proof for theBenchmark
% See solution above
% 23.65/4.32 % (1707213)------------------------------
% 23.65/4.32 % (1707213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.65/4.32 % (1707213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.65/4.32 % (1707213)CaDiCaL version: 2.1.3
% 23.65/4.32 % (1707213)Termination reason: Refutation
% 23.65/4.32 % (1707213)Time elapsed: 3.0000 s
% 23.65/4.32 % (1707213)Peak memory usage: 175 MB
% 23.65/4.32 % (1707213)Instructions burned: 9886 (million)
% 23.65/4.32 % (1707213)------------------------------
% 23.65/4.32 % (1707213)------------------------------
% 23.65/4.32 % (1707208)Success in time 3.274 s
% 23.65/4.32 % Vampire exiting
%------------------------------------------------------------------------------