%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO333+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:29 AM UTC 2026
% Result : Theorem 15.10s 3.32s
% Output : Refutation 18.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 33
% Syntax : Number of formulae : 388 ( 61 unt; 14 def)
% Number of atoms : 2353 ( 843 equ)
% Maximal formula atoms : 26 ( 6 avg)
% Number of connectives : 3379 (1414 ~;1843 |; 97 &)
% ( 18 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 13 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-3 aty)
% Number of variables : 798 ( 0 sgn 770 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vangle(vd1371,vd1362,vd1363) = vangle(vd1361,vd1363,vd1362),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(391), 1375, 0)') ).
fof(f2,negated_conjecture,
vangle(vd1371,vd1362,vd1363) != vangle(vd1361,vd1363,vd1362),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f4,axiom,
vf(vd1362,vd1371) = vf(vd1361,vd1363),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(390), 1373, 0)') ).
fof(f5,axiom,
rR(vd1371,vd1362,vd1361),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(390), 1372, 0)') ).
fof(f6,axiom,
rpoint(vd1371),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(390, 0)') ).
fof(f7,axiom,
? [X0] :
( vd1362 = X0
& rpoint(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(s2(plural(386)))') ).
fof(f9,axiom,
vangle(vd1361,vd1362,vd1363) = vangle(vd1361,vd1363,vd1362),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(386, 1365, 0)') ).
fof(f10,axiom,
vd1362 != vd1363,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(386, 9)') ).
fof(f11,axiom,
vd1361 != vd1363,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(386, 8)') ).
fof(f12,axiom,
vd1361 != vd1362,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(386, 7)') ).
fof(f13,axiom,
? [X0] :
( vd1363 = X0
& rpoint(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(s3(plural(386)))') ).
fof(f14,axiom,
? [X0] :
( vd1361 = X0
& rpoint(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(s1(plural(386)))') ).
fof(f26,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(f30,axiom,
! [X0,X1] :
( ( ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ( vf(X0,X1) = v0
<=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))') ).
fof(f38,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(f45,axiom,
v0 = vd684,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(axiom(137), 2)') ).
fof(f52,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(f55,axiom,
! [X0,X1] :
( ( X0 != X1
& ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ? [X4] :
( ron(X1,X4)
& ron(X0,X4)
& rline(X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(51), 0), imp(cond(axiom(51), 0)))') ).
fof(f82,axiom,
! [X0,X1,X2,X3] :
( ( rR(X3,X0,X1)
& rR(X1,X0,X2)
& ? [X4] :
( X3 = X4
& rpoint(X4) )
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> rR(X3,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(87), 0), imp(cond(axiom(87), 0)))') ).
fof(f119,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(f131,plain,
vangle(vd1371,vd1362,vd1363) != vangle(vd1361,vd1363,vd1362),
inference(flattening,[],[f2]) ).
fof(f156,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,[],[f26]) ).
fof(f157,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,[],[f156]) ).
fof(f162,plain,
! [X0,X1] :
( ( vf(X0,X1) = v0
<=> X0 = X1 )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f30]) ).
fof(f163,plain,
! [X0,X1] :
( ( vf(X0,X1) = v0
<=> X0 = X1 )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f162]) ).
fof(f178,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,[],[f38]) ).
fof(f179,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,[],[f178]) ).
fof(f202,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,[],[f52]) ).
fof(f203,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,[],[f202]) ).
fof(f208,plain,
! [X0,X1] :
( ? [X4] :
( ron(X1,X4)
& ron(X0,X4)
& rline(X4) )
| X0 = X1
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f55]) ).
fof(f209,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,[],[f208]) ).
fof(f261,plain,
! [X0,X1,X2,X3] :
( rR(X3,X0,X2)
| ~ rR(X3,X0,X1)
| ~ rR(X1,X0,X2)
| ! [X4] :
( X3 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f82]) ).
fof(f262,plain,
! [X0,X1,X2,X3] :
( rR(X3,X0,X2)
| ~ rR(X3,X0,X1)
| ~ rR(X1,X0,X2)
| ! [X4] :
( X3 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f261]) ).
fof(f330,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,[],[f119]) ).
fof(f331,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,[],[f330]) ).
fof(f352,plain,
( vd1362 = sK1
& rpoint(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X0,sK1)],[f7]) ).
fof(f353,plain,
( vd1363 = sK2
& rpoint(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2)],[f13]) ).
fof(f354,plain,
( vd1361 = sK3
& rpoint(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X0,sK3)],[f14]) ).
fof(f362,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,[],[f157]) ).
fof(f363,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,[],[f362]) ).
fof(f366,plain,
! [X0,X1] :
( ( ( vf(X0,X1) = v0
| X0 != X1 )
& ( X0 = X1
| vf(X0,X1) != v0 ) )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(nnf_transformation,[],[f163]) ).
fof(f374,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,[],[f209]) ).
fof(f375,plain,
! [X0,X1] :
( ( ron(X1,sK10(X0,X1))
& ron(X0,sK10(X0,X1))
& rline(sK10(X0,X1)) )
| X0 = X1
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X2,sK10(X0,X1))],[f374]) ).
fof(f432,plain,
vangle(vd1371,vd1362,vd1363) != vangle(vd1361,vd1363,vd1362),
inference(cnf_transformation,[],[f131]) ).
fof(f434,plain,
vf(vd1361,vd1363) = vf(vd1362,vd1371),
inference(cnf_transformation,[],[f4]) ).
fof(f435,plain,
rR(vd1371,vd1362,vd1361),
inference(cnf_transformation,[],[f5]) ).
fof(f436,plain,
rpoint(vd1371),
inference(cnf_transformation,[],[f6]) ).
fof(f437,plain,
rpoint(sK1),
inference(cnf_transformation,[],[f352]) ).
fof(f438,plain,
vd1362 = sK1,
inference(cnf_transformation,[],[f352]) ).
fof(f440,plain,
vangle(vd1361,vd1363,vd1362) = vangle(vd1361,vd1362,vd1363),
inference(cnf_transformation,[],[f9]) ).
fof(f441,plain,
vd1362 != vd1363,
inference(cnf_transformation,[],[f10]) ).
fof(f442,plain,
vd1363 != vd1361,
inference(cnf_transformation,[],[f11]) ).
fof(f443,plain,
vd1362 != vd1361,
inference(cnf_transformation,[],[f12]) ).
fof(f444,plain,
rpoint(sK2),
inference(cnf_transformation,[],[f353]) ).
fof(f445,plain,
vd1363 = sK2,
inference(cnf_transformation,[],[f353]) ).
fof(f446,plain,
rpoint(sK3),
inference(cnf_transformation,[],[f354]) ).
fof(f447,plain,
vd1361 = sK3,
inference(cnf_transformation,[],[f354]) ).
fof(f470,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,[],[f363]) ).
fof(f471,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,[],[f363]) ).
fof(f472,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,[],[f363]) ).
fof(f477,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| vf(X0,X1) != v0
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f366]) ).
fof(f478,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = v0
| X0 != X1
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f366]) ).
fof(f487,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,[],[f179]) ).
fof(f488,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,[],[f179]) ).
fof(f489,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,[],[f179]) ).
fof(f490,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,[],[f179]) ).
fof(f497,plain,
v0 = vd684,
inference(cnf_transformation,[],[f45]) ).
fof(f507,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,[],[f203]) ).
fof(f512,plain,
! [X3,X0,X1,X4] :
( rline(sK10(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f375]) ).
fof(f513,plain,
! [X3,X0,X1,X4] :
( ron(X0,sK10(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f375]) ).
fof(f514,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK10(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f375]) ).
fof(f555,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( rR(X3,X0,X2)
| ~ rR(X3,X0,X1)
| ~ rR(X1,X0,X2)
| X3 != X4
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f262]) ).
fof(f680,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,[],[f331]) ).
fof(f696,plain,
vangle(vd1371,sK1,sK2) != vangle(sK3,sK2,sK1),
inference(definition_unfolding,[],[f432,f438,f445,f447,f445,f438]) ).
fof(f698,plain,
vf(sK3,sK2) = vf(sK1,vd1371),
inference(definition_unfolding,[],[f434,f447,f445,f438]) ).
fof(f699,plain,
rR(vd1371,sK1,sK3),
inference(definition_unfolding,[],[f435,f438,f447]) ).
fof(f700,plain,
vangle(sK3,sK2,sK1) = vangle(sK3,sK1,sK2),
inference(definition_unfolding,[],[f440,f447,f445,f438,f447,f438,f445]) ).
fof(f701,plain,
sK1 != sK2,
inference(definition_unfolding,[],[f441,f438,f445]) ).
fof(f702,plain,
sK2 != sK3,
inference(definition_unfolding,[],[f442,f445,f447]) ).
fof(f703,plain,
sK1 != sK3,
inference(definition_unfolding,[],[f443,f438,f447]) ).
fof(f706,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,[],[f472,f497]) ).
fof(f707,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,[],[f471,f497]) ).
fof(f708,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,[],[f470,f497]) ).
fof(f709,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = vd684
| X0 != X1
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(definition_unfolding,[],[f478,f497]) ).
fof(f710,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| vf(X0,X1) != vd684
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(definition_unfolding,[],[f477,f497]) ).
fof(f829,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,[],[f706]) ).
fof(f830,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,[],[f829]) ).
fof(f831,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,[],[f830]) ).
fof(f832,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,[],[f831]) ).
fof(f833,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,[],[f707]) ).
fof(f834,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,[],[f833]) ).
fof(f835,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,[],[f834]) ).
fof(f836,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,[],[f835]) ).
fof(f837,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,[],[f708]) ).
fof(f838,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,[],[f837]) ).
fof(f839,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,[],[f838]) ).
fof(f840,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,[],[f839]) ).
fof(f849,plain,
! [X2,X3,X1] :
( vd684 = vf(X1,X1)
| X1 != X2
| ~ rpoint(X2)
| X1 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f709]) ).
fof(f850,plain,
! [X2,X3] :
( vd684 = vf(X2,X2)
| ~ rpoint(X2)
| X2 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f849]) ).
fof(f851,plain,
! [X3] :
( vd684 = vf(X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f850]) ).
fof(f852,plain,
! [X2,X3,X0] :
( X0 = X2
| vf(X0,X2) != vd684
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f710]) ).
fof(f853,plain,
! [X2,X3] :
( vd684 != vf(X3,X2)
| X2 = X3
| ~ rpoint(X2)
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f852]) ).
fof(f876,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,[],[f490]) ).
fof(f877,plain,
! [X3,X0,X4,X5] :
( ~ rR(X0,X4,X3)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f876]) ).
fof(f878,plain,
! [X3,X4,X5] :
( ~ rR(X5,X4,X3)
| ~ rR(X4,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f877]) ).
fof(f879,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,[],[f489]) ).
fof(f880,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X3,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f879]) ).
fof(f881,plain,
! [X3,X4,X5] :
( ~ rR(X4,X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f880]) ).
fof(f882,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f881]) ).
fof(f883,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,[],[f488]) ).
fof(f884,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X1,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X1 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f883]) ).
fof(f885,plain,
! [X3,X4,X5] :
( ~ rR(X4,X4,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X4 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f884]) ).
fof(f886,plain,
! [X3,X5] :
( ~ rR(X5,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f885]) ).
fof(f887,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,[],[f487]) ).
fof(f888,plain,
! [X3,X0,X4,X5] :
( rR(X4,X3,X0)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f887]) ).
fof(f889,plain,
! [X3,X4,X5] :
( ~ rR(X4,X5,X3)
| rR(X4,X3,X5)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f888]) ).
fof(f932,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,[],[f507]) ).
fof(f933,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,[],[f932]) ).
fof(f934,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,[],[f933]) ).
fof(f935,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,[],[f934]) ).
fof(f936,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,[],[f935]) ).
fof(f937,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,[],[f936]) ).
fof(f938,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,[],[f937]) ).
fof(f948,plain,
! [X3,X0,X4] :
( ron(X3,sK10(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f514]) ).
fof(f949,plain,
! [X3,X4] :
( ron(X3,sK10(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f948]) ).
fof(f950,plain,
! [X3,X0,X4] :
( ron(X0,sK10(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f513]) ).
fof(f951,plain,
! [X3,X4] :
( ron(X4,sK10(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f950]) ).
fof(f952,plain,
! [X3,X0,X4] :
( rline(sK10(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f512]) ).
fof(f953,plain,
! [X3,X4] :
( rline(sK10(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f952]) ).
fof(f1100,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( rR(X4,X0,X2)
| ~ rR(X4,X0,X1)
| ~ rR(X1,X0,X2)
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f555]) ).
fof(f1101,plain,
! [X0,X1,X6,X7,X4,X5] :
( rR(X4,X0,X5)
| ~ rR(X4,X0,X1)
| ~ rR(X1,X0,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1100]) ).
fof(f1102,plain,
! [X0,X6,X7,X4,X5] :
( rR(X4,X0,X5)
| ~ rR(X4,X0,X6)
| ~ rR(X6,X0,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1101]) ).
fof(f1103,plain,
! [X6,X7,X4,X5] :
( ~ rR(X6,X7,X5)
| ~ rR(X4,X7,X6)
| rR(X4,X7,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1102]) ).
fof(f1426,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,[],[f680]) ).
fof(f1427,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,[],[f1426]) ).
fof(f1428,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,[],[f1427]) ).
fof(f1495,definition,
sF52 = vangle(vd1371,sK1,sK2),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f1496,plain,
vangle(vd1371,sK1,sK2) = sF52,
inference(reorient_equations,[],[f1495]) ).
fof(f1497,definition,
sF53 = vangle(sK3,sK2,sK1),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f1498,plain,
vangle(sK3,sK2,sK1) = sF53,
inference(reorient_equations,[],[f1497]) ).
fof(f1499,plain,
sF52 != sF53,
inference(definition_folding,[],[f696,f1498,f1496]) ).
fof(f1500,plain,
! [X3,X5] :
( ~ rR(X5,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X5) ),
inference(duplicate_literal_removal,[],[f886]) ).
fof(f1501,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f882]) ).
fof(f1502,plain,
! [X3] :
( ~ rpoint(X3)
| vd684 = vf(X3,X3) ),
inference(duplicate_literal_removal,[],[f851]) ).
fof(f1550,plain,
vangle(sK3,sK1,sK2) = sF53,
inference(forward_demodulation,[],[f1498,f700]) ).
fof(f1553,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK2 = X1
| ~ rpoint(X0)
| sK2 = X0
| vangle(X0,X1,sK2) = vangle(sK2,X1,X0) ),
inference(resolution,[],[f1428,f444]) ).
fof(f1554,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK3 = X1
| ~ rpoint(X0)
| sK3 = X0
| vangle(X0,X1,sK3) = vangle(sK3,X1,X0) ),
inference(resolution,[],[f1428,f446]) ).
fof(f1555,plain,
( rR(vd1371,sK3,sK1)
| ~ rpoint(sK3)
| ~ rpoint(vd1371)
| ~ rpoint(sK1) ),
inference(resolution,[],[f889,f699]) ).
fof(f1556,plain,
( rR(vd1371,sK3,sK1)
| ~ rpoint(vd1371)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f1555,f446]) ).
fof(f1557,plain,
( rR(vd1371,sK3,sK1)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f1556,f436]) ).
fof(f1558,plain,
rR(vd1371,sK3,sK1),
inference(forward_subsumption_resolution,[],[f1557,f437]) ).
fof(f1567,definition,
( spl54_13
<=> vd1371 = sK1 ),
introduced(definition,[new_symbols(definition,[spl54_13])],[avatar_definition]) ).
fof(f1568,plain,
( vd1371 != sK1
| spl54_13 ),
inference(avatar_component_clause,[],[f1567]) ).
fof(f1569,plain,
( vd1371 = sK1
| ~ spl54_13 ),
inference(avatar_component_clause,[],[f1567]) ).
fof(f1571,definition,
( spl54_14
<=> vd684 = vf(sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl54_14])],[avatar_definition]) ).
fof(f1572,plain,
( vd684 = vf(sK3,sK2)
| ~ spl54_14 ),
inference(avatar_component_clause,[],[f1571]) ).
fof(f1573,plain,
( vd684 != vf(sK3,sK2)
| spl54_14 ),
inference(avatar_component_clause,[],[f1571]) ).
fof(f1608,plain,
( vf(sK3,sK2) = vf(sK1,sK1)
| ~ spl54_13 ),
inference(superposition,[],[f698,f1569]) ).
fof(f1622,plain,
vd684 = vf(vd1371,vd1371),
inference(resolution,[],[f1502,f436]) ).
fof(f1627,plain,
( vd684 = vf(sK1,sK1)
| ~ spl54_13 ),
inference(forward_demodulation,[],[f1622,f1569]) ).
fof(f1630,plain,
( vd684 = vf(sK3,sK2)
| ~ spl54_13 ),
inference(forward_demodulation,[],[f1627,f1608]) ).
fof(f1631,plain,
( $false
| ~ spl54_13
| spl54_14 ),
inference(forward_subsumption_resolution,[],[f1630,f1573]) ).
fof(f1632,plain,
( ~ spl54_13
| spl54_14 ),
inference(avatar_contradiction_clause,[],[f1631]) ).
fof(f1638,plain,
( vd684 != vd684
| sK2 = sK3
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ spl54_14 ),
inference(superposition,[],[f853,f1572]) ).
fof(f1639,plain,
( sK2 = sK3
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ spl54_14 ),
inference(trivial_inequality_removal,[],[f1638]) ).
fof(f1640,plain,
( ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ spl54_14 ),
inference(forward_subsumption_resolution,[],[f1639,f702]) ).
fof(f1641,plain,
( ~ rpoint(sK3)
| ~ spl54_14 ),
inference(forward_subsumption_resolution,[],[f1640,f444]) ).
fof(f1642,plain,
( $false
| ~ spl54_14 ),
inference(forward_subsumption_resolution,[],[f1641,f446]) ).
fof(f1643,plain,
~ spl54_14,
inference(avatar_contradiction_clause,[],[f1642]) ).
fof(f1677,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X0,X2,X3)
| rR(X0,X4,X5)
| X0 = X3
| X0 = X5
| X0 = X2
| X0 = X4
| ~ ron(X3,X6)
| ~ ron(X2,X6)
| ~ ron(X5,sK10(X1,X0))
| ~ ron(X4,sK10(X1,X0))
| vangle(X5,X0,X3) = vangle(X4,X0,X2)
| ~ rline(X6)
| ~ rline(sK10(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X0) ),
inference(resolution,[],[f949,f938]) ).
fof(f1678,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X0,X2,X3)
| rR(X0,X4,X5)
| X0 = X3
| X0 = X5
| X0 = X2
| X0 = X4
| ~ ron(X3,X6)
| ~ ron(X2,X6)
| ~ ron(X5,sK10(X1,X0))
| ~ ron(X4,sK10(X1,X0))
| vangle(X5,X0,X3) = vangle(X4,X0,X2)
| ~ rline(X6)
| ~ rline(sK10(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f1677]) ).
fof(f1679,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ ron(X5,sK10(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X0,X2,X3)
| rR(X0,X4,X5)
| X0 = X3
| X0 = X5
| X0 = X2
| X0 = X4
| ~ ron(X3,X6)
| ~ ron(X2,X6)
| X0 = X1
| ~ ron(X4,sK10(X1,X0))
| vangle(X5,X0,X3) = vangle(X4,X0,X2)
| ~ rline(X6)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(forward_subsumption_resolution,[],[f1678,f953]) ).
fof(f1680,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,sK10(X1,X0))
| ~ ron(X4,sK10(X1,X0))
| vangle(X5,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X6)
| ~ rline(sK10(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1) ),
inference(resolution,[],[f951,f938]) ).
fof(f1681,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,sK10(X1,X0))
| ~ ron(X4,sK10(X1,X0))
| vangle(X5,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X6)
| ~ rline(sK10(X1,X0))
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f1680]) ).
fof(f1682,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ ron(X5,sK10(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,sK10(X1,X0))
| vangle(X5,X1,X3) = vangle(X4,X1,X2)
| ~ rline(X6)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(forward_subsumption_resolution,[],[f1681,f953]) ).
fof(f1684,plain,
! [X0] :
( sK1 = sK3
| ~ rpoint(X0)
| sK3 = X0
| vangle(X0,sK1,sK3) = vangle(sK3,sK1,X0) ),
inference(resolution,[],[f1554,f437]) ).
fof(f1688,plain,
! [X0] :
( ~ rpoint(X0)
| sK3 = X0
| vangle(X0,sK1,sK3) = vangle(sK3,sK1,X0) ),
inference(forward_subsumption_resolution,[],[f1684,f703]) ).
fof(f1693,definition,
( spl54_23
<=> vd1371 = sK3 ),
introduced(definition,[new_symbols(definition,[spl54_23])],[avatar_definition]) ).
fof(f1694,plain,
( vd1371 != sK3
| spl54_23 ),
inference(avatar_component_clause,[],[f1693]) ).
fof(f1695,plain,
( vd1371 = sK3
| ~ spl54_23 ),
inference(avatar_component_clause,[],[f1693]) ).
fof(f1714,plain,
( vangle(sK3,sK1,sK2) = sF52
| ~ spl54_23 ),
inference(superposition,[],[f1496,f1695]) ).
fof(f1718,plain,
( sF52 = sF53
| ~ spl54_23 ),
inference(forward_demodulation,[],[f1714,f1550]) ).
fof(f1721,plain,
( $false
| ~ spl54_23 ),
inference(forward_subsumption_resolution,[],[f1718,f1499]) ).
fof(f1722,plain,
~ spl54_23,
inference(avatar_contradiction_clause,[],[f1721]) ).
fof(f1725,plain,
( sK2 = sK3
| vangle(sK3,sK1,sK2) = vangle(sK2,sK1,sK3) ),
inference(resolution,[],[f1688,f444]) ).
fof(f1727,plain,
vangle(sK3,sK1,sK2) = vangle(sK2,sK1,sK3),
inference(forward_subsumption_resolution,[],[f1725,f702]) ).
fof(f1730,plain,
sF53 = vangle(sK2,sK1,sK3),
inference(forward_demodulation,[],[f1727,f1550]) ).
fof(f1731,plain,
! [X2,X3,X0,X1] :
( rR(X0,X1,X2)
| vangle(X1,X0,X2) = vd684
| ~ ron(X1,sK10(X3,X2))
| ~ ron(X0,sK10(X3,X2))
| X0 = X2
| X0 = X1
| ~ rline(sK10(X3,X2))
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| X2 = X3
| ~ rpoint(X2)
| ~ rpoint(X3) ),
inference(resolution,[],[f840,f949]) ).
fof(f1734,plain,
! [X2,X3,X0,X1] :
( rR(X0,X1,X2)
| vangle(X1,X0,X2) = vd684
| ~ ron(X1,sK10(X3,X2))
| ~ ron(X0,sK10(X3,X2))
| X0 = X2
| X0 = X1
| ~ rline(sK10(X3,X2))
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| X2 = X3
| ~ rpoint(X3) ),
inference(duplicate_literal_removal,[],[f1731]) ).
fof(f1736,plain,
! [X2,X3,X0,X1] :
( ~ ron(X1,sK10(X3,X2))
| vangle(X1,X0,X2) = vd684
| rR(X0,X1,X2)
| ~ ron(X0,sK10(X3,X2))
| X0 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| X2 = X3
| ~ rpoint(X3) ),
inference(forward_subsumption_resolution,[],[f1734,f953]) ).
fof(f1737,plain,
! [X2,X0,X1] :
( vd684 = vangle(X0,X1,X0)
| rR(X1,X0,X0)
| ~ ron(X1,sK10(X2,X0))
| X0 = X1
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X2
| ~ rpoint(X2)
| X0 = X2
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(resolution,[],[f1736,f949]) ).
fof(f1740,plain,
! [X2,X0,X1] :
( vd684 = vangle(X0,X1,X0)
| rR(X1,X0,X0)
| ~ ron(X1,sK10(X2,X0))
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X2
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f1737]) ).
fof(f1741,plain,
! [X2,X0,X1] :
( ~ ron(X1,sK10(X2,X0))
| vd684 = vangle(X0,X1,X0)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X2
| ~ rpoint(X2) ),
inference(forward_subsumption_resolution,[],[f1740,f1501]) ).
fof(f1747,plain,
! [X0,X1] :
( vd684 = vangle(X0,X1,X0)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1
| ~ rpoint(X1)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f1741,f951]) ).
fof(f1748,plain,
! [X0,X1] :
( ~ rpoint(X1)
| X0 = X1
| ~ rpoint(X0)
| vd684 = vangle(X0,X1,X0) ),
inference(duplicate_literal_removal,[],[f1747]) ).
fof(f1751,plain,
! [X0] :
( ~ rpoint(X0)
| sK1 = X0
| vd684 = vangle(X0,sK1,X0) ),
inference(resolution,[],[f1748,f437]) ).
fof(f1752,plain,
! [X0] :
( ~ rpoint(X0)
| sK2 = X0
| vd684 = vangle(X0,sK2,X0) ),
inference(resolution,[],[f1748,f444]) ).
fof(f1763,plain,
( sK1 = sK2
| vd684 = vangle(sK2,sK1,sK2) ),
inference(resolution,[],[f1751,f444]) ).
fof(f1766,plain,
vd684 = vangle(sK2,sK1,sK2),
inference(forward_subsumption_resolution,[],[f1763,f701]) ).
fof(f1771,plain,
( sK2 = sK3
| vd684 = vangle(sK3,sK2,sK3) ),
inference(resolution,[],[f1752,f446]) ).
fof(f1772,plain,
vd684 = vangle(sK3,sK2,sK3),
inference(forward_subsumption_resolution,[],[f1771,f702]) ).
fof(f1779,definition,
( spl54_26
<=> vd1371 = sK2 ),
introduced(definition,[new_symbols(definition,[spl54_26])],[avatar_definition]) ).
fof(f1780,plain,
( vd1371 != sK2
| spl54_26 ),
inference(avatar_component_clause,[],[f1779]) ).
fof(f1781,plain,
( vd1371 = sK2
| ~ spl54_26 ),
inference(avatar_component_clause,[],[f1779]) ).
fof(f1806,plain,
( sF52 = vangle(sK2,sK1,sK2)
| ~ spl54_26 ),
inference(superposition,[],[f1496,f1781]) ).
fof(f1810,plain,
( vd684 = sF52
| ~ spl54_26 ),
inference(forward_demodulation,[],[f1806,f1766]) ).
fof(f1814,plain,
! [X0] :
( sK1 = sK2
| ~ rpoint(X0)
| sK2 = X0
| vangle(X0,sK1,sK2) = vangle(sK2,sK1,X0) ),
inference(resolution,[],[f1553,f437]) ).
fof(f1818,plain,
! [X0] :
( ~ rpoint(X0)
| sK2 = X0
| vangle(X0,sK1,sK2) = vangle(sK2,sK1,X0) ),
inference(forward_subsumption_resolution,[],[f1814,f701]) ).
fof(f1825,plain,
( vd1371 = sK2
| vangle(vd1371,sK1,sK2) = vangle(sK2,sK1,vd1371) ),
inference(resolution,[],[f1818,f436]) ).
fof(f1878,plain,
! [X0] :
( vd684 != sF53
| ~ rR(sK1,sK3,sK2)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| sK1 = sK2
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(superposition,[],[f832,f1550]) ).
fof(f1907,plain,
! [X0] :
( vd684 != sF53
| ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| sK1 = sK2
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) ),
inference(superposition,[],[f836,f1550]) ).
fof(f1933,plain,
! [X0] :
( ~ rR(X0,sK3,vd1371)
| rR(X0,sK3,sK1)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ rpoint(sK3) ),
inference(resolution,[],[f1103,f1558]) ).
fof(f1938,plain,
! [X0] :
( ~ rR(X0,sK3,vd1371)
| rR(X0,sK3,sK1)
| ~ rpoint(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1933,f437]) ).
fof(f1942,plain,
! [X0] :
( ~ rR(X0,sK3,vd1371)
| rR(X0,sK3,sK1)
| ~ rpoint(X0)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f1938,f436]) ).
fof(f1946,plain,
! [X0] :
( ~ rR(X0,sK3,vd1371)
| rR(X0,sK3,sK1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f1942,f446]) ).
fof(f3992,plain,
( vangle(vd1371,sK1,sK2) = vangle(sK2,sK1,vd1371)
| spl54_26 ),
inference(forward_subsumption_resolution,[],[f1825,f1780]) ).
fof(f4086,plain,
( sF52 = vangle(sK2,sK1,vd1371)
| spl54_26 ),
inference(forward_demodulation,[],[f3992,f1496]) ).
fof(f7237,definition,
( spl54_379
<=> sF53 = vangle(sK3,sK1,vd1371) ),
introduced(definition,[new_symbols(definition,[spl54_379])],[avatar_definition]) ).
fof(f7238,plain,
( sF53 != vangle(sK3,sK1,vd1371)
| spl54_379 ),
inference(avatar_component_clause,[],[f7237]) ).
fof(f7239,plain,
( sF53 = vangle(sK3,sK1,vd1371)
| ~ spl54_379 ),
inference(avatar_component_clause,[],[f7237]) ).
fof(f11965,definition,
( spl54_677
<=> vd684 = sF53 ),
introduced(definition,[new_symbols(definition,[spl54_677])],[avatar_definition]) ).
fof(f11966,plain,
( vd684 != sF53
| spl54_677 ),
inference(avatar_component_clause,[],[f11965]) ).
fof(f11967,plain,
( vd684 = sF53
| ~ spl54_677 ),
inference(avatar_component_clause,[],[f11965]) ).
fof(f13867,definition,
( spl54_881
<=> vd684 = sF52 ),
introduced(definition,[new_symbols(definition,[spl54_881])],[avatar_definition]) ).
fof(f13868,plain,
( vd684 = sF52
| ~ spl54_881 ),
inference(avatar_component_clause,[],[f13867]) ).
fof(f13869,plain,
( vd684 != sF52
| spl54_881 ),
inference(avatar_component_clause,[],[f13867]) ).
fof(f14006,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| rR(X0,X2,X3)
| rR(X0,X4,X1)
| X0 = X3
| X0 = X1
| X0 = X2
| X0 = X4
| ~ ron(X3,X5)
| ~ ron(X2,X5)
| X0 = X1
| ~ ron(X4,sK10(X1,X0))
| vangle(X1,X0,X3) = vangle(X4,X0,X2)
| ~ rline(X5)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X4)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f1679,f951]) ).
fof(f14007,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ ron(X4,sK10(X1,X0))
| ~ rpoint(X1)
| rR(X0,X2,X3)
| rR(X0,X4,X1)
| X0 = X3
| X0 = X1
| X0 = X2
| X0 = X4
| ~ ron(X3,X5)
| ~ ron(X2,X5)
| ~ rpoint(X0)
| vangle(X1,X0,X3) = vangle(X4,X0,X2)
| ~ rline(X5)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f14006]) ).
fof(f14009,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,sK10(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,[],[f1682,f949]) ).
fof(f14012,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ ron(X4,sK10(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,[],[f14009]) ).
fof(f14013,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,[],[f14012,f949]) ).
fof(f14016,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,[],[f14013]) ).
fof(f14017,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,[],[f14016,f1501]) ).
fof(f14018,plain,
! [X2,X3,X0,X1,X4] :
( rR(X0,X1,X2)
| X0 = X2
| X0 = X3
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,sK10(X4,X2))
| ~ rpoint(X3)
| vangle(X3,X0,X2) = vangle(X3,X0,X1)
| ~ rline(sK10(X4,X2))
| ~ rpoint(X2)
| ~ rpoint(X1)
| X2 = X4
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(resolution,[],[f14017,f949]) ).
fof(f14061,plain,
! [X2,X3,X0,X1,X4] :
( rR(X0,X1,X2)
| X0 = X2
| X0 = X3
| X0 = X1
| ~ rpoint(X0)
| ~ ron(X1,sK10(X4,X2))
| ~ rpoint(X3)
| vangle(X3,X0,X2) = vangle(X3,X0,X1)
| ~ rline(sK10(X4,X2))
| ~ rpoint(X2)
| ~ rpoint(X1)
| X2 = X4
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f14018]) ).
fof(f14063,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X1,sK10(X4,X2))
| X0 = X2
| X0 = X3
| X0 = X1
| ~ rpoint(X0)
| rR(X0,X1,X2)
| ~ rpoint(X3)
| vangle(X3,X0,X2) = vangle(X3,X0,X1)
| ~ rpoint(X2)
| ~ rpoint(X1)
| X2 = X4
| ~ rpoint(X4) ),
inference(forward_subsumption_resolution,[],[f14061,f953]) ).
fof(f14069,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| X0 = X2
| X0 = X3
| ~ rpoint(X0)
| rR(X0,X3,X1)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,X3)
| ~ rpoint(X1)
| ~ rpoint(X3)
| X1 = X3
| ~ rpoint(X3)
| X1 = X3
| ~ rpoint(X1)
| ~ rpoint(X3) ),
inference(resolution,[],[f14063,f951]) ).
fof(f14070,plain,
! [X2,X3,X0,X1] :
( ~ rpoint(X3)
| X0 = X2
| X0 = X3
| ~ rpoint(X0)
| rR(X0,X3,X1)
| ~ rpoint(X2)
| vangle(X2,X0,X1) = vangle(X2,X0,X3)
| ~ rpoint(X1)
| X0 = X1
| X1 = X3 ),
inference(duplicate_literal_removal,[],[f14069]) ).
fof(f14083,plain,
! [X2,X0,X1] :
( ~ rpoint(X2)
| sK1 = X0
| ~ rpoint(X0)
| rR(X0,sK1,X2)
| ~ rpoint(X1)
| vangle(X1,X0,X2) = vangle(X1,X0,sK1)
| X0 = X1
| X0 = X2
| sK1 = X2 ),
inference(resolution,[],[f14070,f437]) ).
fof(f14084,plain,
! [X2,X0,X1] :
( ~ rpoint(X2)
| sK2 = X0
| ~ rpoint(X0)
| rR(X0,sK2,X2)
| ~ rpoint(X1)
| vangle(X1,X0,X2) = vangle(X1,X0,sK2)
| X0 = X1
| X0 = X2
| sK2 = X2 ),
inference(resolution,[],[f14070,f444]) ).
fof(f14129,plain,
! [X0,X1] :
( sK1 = X0
| ~ rpoint(X0)
| rR(X0,sK1,sK3)
| ~ rpoint(X1)
| vangle(X1,X0,sK3) = vangle(X1,X0,sK1)
| X0 = X1
| sK3 = X0
| sK1 = sK3 ),
inference(resolution,[],[f14083,f446]) ).
fof(f14131,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| rR(X0,sK1,sK3)
| sK1 = X0
| vangle(X1,X0,sK3) = vangle(X1,X0,sK1)
| X0 = X1
| sK3 = X0 ),
inference(forward_subsumption_resolution,[],[f14129,f703]) ).
fof(f14155,plain,
! [X0,X1] :
( sK2 = X0
| ~ rpoint(X0)
| rR(X0,sK2,sK3)
| ~ rpoint(X1)
| vangle(X1,X0,sK3) = vangle(X1,X0,sK2)
| X0 = X1
| sK3 = X0
| sK2 = sK3 ),
inference(resolution,[],[f14084,f446]) ).
fof(f14157,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| rR(X0,sK2,sK3)
| sK2 = X0
| vangle(X1,X0,sK3) = vangle(X1,X0,sK2)
| X0 = X1
| sK3 = X0 ),
inference(forward_subsumption_resolution,[],[f14155,f702]) ).
fof(f14212,plain,
! [X0] :
( ~ rpoint(X0)
| rR(X0,sK2,sK3)
| sK2 = X0
| vangle(sK2,X0,sK2) = vangle(sK2,X0,sK3)
| sK2 = X0
| sK3 = X0 ),
inference(resolution,[],[f14157,f444]) ).
fof(f14215,plain,
! [X0] :
( rR(X0,sK2,sK3)
| ~ rpoint(X0)
| sK2 = X0
| vangle(sK2,X0,sK2) = vangle(sK2,X0,sK3)
| sK3 = X0 ),
inference(duplicate_literal_removal,[],[f14212]) ).
fof(f14229,plain,
! [X0] :
( ~ rpoint(X0)
| rR(X0,sK1,sK3)
| sK1 = X0
| vangle(sK3,X0,sK3) = vangle(sK3,X0,sK1)
| sK3 = X0
| sK3 = X0 ),
inference(resolution,[],[f14131,f446]) ).
fof(f14230,plain,
! [X0] :
( rR(X0,sK1,sK3)
| ~ rpoint(X0)
| sK1 = X0
| vangle(sK3,X0,sK3) = vangle(sK3,X0,sK1)
| sK3 = X0 ),
inference(duplicate_literal_removal,[],[f14229]) ).
fof(f14338,plain,
( ! [X0] :
( ~ rR(sK1,sK3,sK2)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| sK1 = sK2
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f1878,f11967]) ).
fof(f14346,plain,
( ! [X0] :
( ~ rR(sK1,sK3,sK2)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f14338,f701]) ).
fof(f14364,plain,
( ! [X0] :
( ~ rR(sK1,sK3,sK2)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f14346,f703]) ).
fof(f14368,plain,
( ! [X0] :
( ~ rR(sK1,sK3,sK2)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f14364,f444]) ).
fof(f14372,plain,
( ! [X0] :
( ~ rR(sK1,sK3,sK2)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK1) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f14368,f446]) ).
fof(f14376,plain,
( ! [X0] :
( ~ rR(sK1,sK3,sK2)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f14372,f437]) ).
fof(f14381,definition,
( spl54_913
<=> ! [X0] :
( ~ ron(sK3,X0)
| ~ rline(X0)
| ~ ron(sK1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_913])],[avatar_definition]) ).
fof(f14382,plain,
( ! [X0] :
( ~ ron(sK3,X0)
| ~ rline(X0)
| ~ ron(sK1,X0) )
| ~ spl54_913 ),
inference(avatar_component_clause,[],[f14381]) ).
fof(f14384,definition,
( spl54_914
<=> rR(sK1,sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl54_914])],[avatar_definition]) ).
fof(f14387,plain,
( spl54_913
| ~ spl54_914
| ~ spl54_677 ),
inference(avatar_split_clause,[],[f14376,f11965,f14384,f14381]) ).
fof(f15166,definition,
( spl54_931
<=> rR(sK1,sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl54_931])],[avatar_definition]) ).
fof(f15167,plain,
( ~ rR(sK1,sK2,sK3)
| spl54_931 ),
inference(avatar_component_clause,[],[f15166]) ).
fof(f15168,plain,
( rR(sK1,sK2,sK3)
| ~ spl54_931 ),
inference(avatar_component_clause,[],[f15166]) ).
fof(f15170,definition,
( spl54_932
<=> ! [X2,X0,X1] :
( rR(sK1,X0,X1)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rline(X2)
| vangle(sK2,sK1,X0) = vangle(sK3,sK1,X1)
| ~ ron(X0,X2)
| ~ ron(X1,X2)
| sK1 = X0
| sK1 = X1 ) ),
introduced(definition,[new_symbols(definition,[spl54_932])],[avatar_definition]) ).
fof(f15171,plain,
( ! [X2,X0,X1] :
( ~ ron(X1,X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rline(X2)
| vangle(sK2,sK1,X0) = vangle(sK3,sK1,X1)
| ~ ron(X0,X2)
| rR(sK1,X0,X1)
| sK1 = X0
| sK1 = X1 )
| ~ spl54_932 ),
inference(avatar_component_clause,[],[f15170]) ).
fof(f15181,definition,
( spl54_933
<=> rR(sK2,sK1,sK3) ),
introduced(definition,[new_symbols(definition,[spl54_933])],[avatar_definition]) ).
fof(f15182,plain,
( ~ rR(sK2,sK1,sK3)
| spl54_933 ),
inference(avatar_component_clause,[],[f15181]) ).
fof(f15183,plain,
( rR(sK2,sK1,sK3)
| ~ spl54_933 ),
inference(avatar_component_clause,[],[f15181]) ).
fof(f15192,plain,
( ~ rR(sK2,sK1,sK3)
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ spl54_931 ),
inference(resolution,[],[f15168,f878]) ).
fof(f15193,plain,
( rR(sK1,sK3,sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ rpoint(sK2)
| ~ spl54_931 ),
inference(resolution,[],[f15168,f889]) ).
fof(f15202,plain,
( rR(sK1,sK3,sK2)
| ~ rpoint(sK1)
| ~ rpoint(sK2)
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f15193,f446]) ).
fof(f15203,plain,
( ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ spl54_931
| ~ spl54_933 ),
inference(forward_subsumption_resolution,[],[f15192,f15183]) ).
fof(f15209,plain,
( rR(sK1,sK3,sK2)
| ~ rpoint(sK2)
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f15202,f437]) ).
fof(f15210,plain,
( ~ rpoint(sK2)
| ~ rpoint(sK1)
| ~ spl54_931
| ~ spl54_933 ),
inference(forward_subsumption_resolution,[],[f15203,f446]) ).
fof(f15216,plain,
( rR(sK1,sK3,sK2)
| ~ spl54_931 ),
inference(forward_subsumption_resolution,[],[f15209,f444]) ).
fof(f15217,plain,
( ~ rpoint(sK1)
| ~ spl54_931
| ~ spl54_933 ),
inference(forward_subsumption_resolution,[],[f15210,f444]) ).
fof(f15220,plain,
( spl54_914
| ~ spl54_931 ),
inference(avatar_split_clause,[],[f15216,f15166,f14384]) ).
fof(f15221,plain,
( $false
| ~ spl54_931
| ~ spl54_933 ),
inference(forward_subsumption_resolution,[],[f15217,f437]) ).
fof(f15222,plain,
( ~ spl54_931
| ~ spl54_933 ),
inference(avatar_contradiction_clause,[],[f15221]) ).
fof(f15268,plain,
( ~ rpoint(sK1)
| sK1 = sK2
| vangle(sK2,sK1,sK3) = vangle(sK2,sK1,sK2)
| sK1 = sK3
| spl54_931 ),
inference(resolution,[],[f15167,f14215]) ).
fof(f15271,plain,
( sK1 = sK2
| vangle(sK2,sK1,sK3) = vangle(sK2,sK1,sK2)
| sK1 = sK3
| spl54_931 ),
inference(forward_subsumption_resolution,[],[f15268,f437]) ).
fof(f15273,plain,
( vangle(sK2,sK1,sK3) = vangle(sK2,sK1,sK2)
| sK1 = sK3
| spl54_931 ),
inference(forward_subsumption_resolution,[],[f15271,f701]) ).
fof(f15275,plain,
( vangle(sK2,sK1,sK3) = vangle(sK2,sK1,sK2)
| spl54_931 ),
inference(forward_subsumption_resolution,[],[f15273,f703]) ).
fof(f15277,plain,
( vd684 = vangle(sK2,sK1,sK3)
| spl54_931 ),
inference(forward_demodulation,[],[f15275,f1766]) ).
fof(f15279,plain,
( vd684 = sF53
| spl54_931 ),
inference(forward_demodulation,[],[f15277,f1730]) ).
fof(f15282,plain,
( $false
| spl54_677
| spl54_931 ),
inference(forward_subsumption_resolution,[],[f15279,f11966]) ).
fof(f15283,plain,
( spl54_677
| spl54_931 ),
inference(avatar_contradiction_clause,[],[f15282]) ).
fof(f15441,plain,
( ! [X0] :
( ~ rline(sK10(sK3,X0))
| ~ ron(sK1,sK10(sK3,X0))
| sK3 = X0
| ~ rpoint(X0)
| ~ rpoint(sK3) )
| ~ spl54_913 ),
inference(resolution,[],[f14382,f951]) ).
fof(f15444,plain,
( ! [X0] :
( ~ ron(sK1,sK10(sK3,X0))
| sK3 = X0
| ~ rpoint(X0)
| ~ rpoint(sK3) )
| ~ spl54_913 ),
inference(forward_subsumption_resolution,[],[f15441,f953]) ).
fof(f15446,plain,
( ! [X0] :
( ~ ron(sK1,sK10(sK3,X0))
| sK3 = X0
| ~ rpoint(X0) )
| ~ spl54_913 ),
inference(forward_subsumption_resolution,[],[f15444,f446]) ).
fof(f15448,plain,
( sK1 = sK3
| ~ rpoint(sK1)
| sK1 = sK3
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ spl54_913 ),
inference(resolution,[],[f15446,f949]) ).
fof(f15449,plain,
( sK1 = sK3
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ spl54_913 ),
inference(duplicate_literal_removal,[],[f15448]) ).
fof(f15450,plain,
( ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ spl54_913 ),
inference(forward_subsumption_resolution,[],[f15449,f703]) ).
fof(f15451,plain,
( ~ rpoint(sK3)
| ~ spl54_913 ),
inference(forward_subsumption_resolution,[],[f15450,f437]) ).
fof(f15452,plain,
( $false
| ~ spl54_913 ),
inference(forward_subsumption_resolution,[],[f15451,f446]) ).
fof(f15453,plain,
~ spl54_913,
inference(avatar_contradiction_clause,[],[f15452]) ).
fof(f15550,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| sK1 = sK2
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f1907,f11967]) ).
fof(f15554,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| sK1 = sK3
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f15550,f701]) ).
fof(f15558,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK2)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f15554,f703]) ).
fof(f15564,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f15558,f444]) ).
fof(f15565,plain,
( ! [X0] :
( ron(sK2,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK1) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f15564,f446]) ).
fof(f15566,plain,
( ! [X0] :
( ~ ron(sK3,X0)
| ron(sK2,X0)
| ~ ron(sK1,X0)
| ~ rline(X0) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f15565,f437]) ).
fof(f15651,plain,
( ~ rpoint(sK2)
| sK1 = sK2
| vangle(sK3,sK2,sK1) = vangle(sK3,sK2,sK3)
| sK2 = sK3
| spl54_933 ),
inference(resolution,[],[f15182,f14230]) ).
fof(f15652,plain,
( sK1 = sK2
| vangle(sK3,sK2,sK1) = vangle(sK3,sK2,sK3)
| sK2 = sK3
| spl54_933 ),
inference(forward_subsumption_resolution,[],[f15651,f444]) ).
fof(f15654,plain,
( vangle(sK3,sK2,sK1) = vangle(sK3,sK2,sK3)
| sK2 = sK3
| spl54_933 ),
inference(forward_subsumption_resolution,[],[f15652,f701]) ).
fof(f15656,plain,
( vangle(sK3,sK2,sK1) = vangle(sK3,sK2,sK3)
| spl54_933 ),
inference(forward_subsumption_resolution,[],[f15654,f702]) ).
fof(f15658,plain,
( vd684 = vangle(sK3,sK2,sK1)
| spl54_933 ),
inference(forward_demodulation,[],[f15656,f1772]) ).
fof(f15660,plain,
( vd684 = vangle(sK3,sK1,sK2)
| spl54_933 ),
inference(forward_demodulation,[],[f15658,f700]) ).
fof(f15662,plain,
( vd684 = sF53
| spl54_933 ),
inference(forward_demodulation,[],[f15660,f1550]) ).
fof(f15709,plain,
( ! [X2,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rline(sK10(X2,X1))
| vangle(sK2,sK1,X0) = vangle(sK3,sK1,X1)
| ~ ron(X0,sK10(X2,X1))
| rR(sK1,X0,X1)
| sK1 = X0
| sK1 = X1
| X1 = X2
| ~ rpoint(X1)
| ~ rpoint(X2) )
| ~ spl54_932 ),
inference(resolution,[],[f15171,f949]) ).
fof(f15752,plain,
( ! [X2,X0,X1] :
( ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rline(sK10(X2,X1))
| vangle(sK2,sK1,X0) = vangle(sK3,sK1,X1)
| ~ ron(X0,sK10(X2,X1))
| rR(sK1,X0,X1)
| sK1 = X0
| sK1 = X1
| X1 = X2
| ~ rpoint(X2) )
| ~ spl54_932 ),
inference(duplicate_literal_removal,[],[f15709]) ).
fof(f15754,plain,
( ! [X2,X0,X1] :
( ~ ron(X0,sK10(X2,X1))
| ~ rpoint(X1)
| vangle(sK2,sK1,X0) = vangle(sK3,sK1,X1)
| ~ rpoint(X0)
| rR(sK1,X0,X1)
| sK1 = X0
| sK1 = X1
| X1 = X2
| ~ rpoint(X2) )
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f15752,f953]) ).
fof(f15755,plain,
( vd684 != sF52
| ~ spl54_677 ),
inference(superposition,[],[f1499,f11967]) ).
fof(f15766,plain,
( ! [X0] :
( ron(sK2,sK10(sK3,X0))
| ~ ron(sK1,sK10(sK3,X0))
| ~ rline(sK10(sK3,X0))
| sK3 = X0
| ~ rpoint(X0)
| ~ rpoint(sK3) )
| ~ spl54_677 ),
inference(resolution,[],[f15566,f951]) ).
fof(f15769,plain,
( ! [X0] :
( ron(sK2,sK10(sK3,X0))
| ~ ron(sK1,sK10(sK3,X0))
| sK3 = X0
| ~ rpoint(X0)
| ~ rpoint(sK3) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f15766,f953]) ).
fof(f15771,plain,
( ! [X0] :
( ~ ron(sK1,sK10(sK3,X0))
| ron(sK2,sK10(sK3,X0))
| sK3 = X0
| ~ rpoint(X0) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f15769,f446]) ).
fof(f15773,plain,
( ron(sK2,sK10(sK3,sK1))
| sK1 = sK3
| ~ rpoint(sK1)
| sK1 = sK3
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ spl54_677 ),
inference(resolution,[],[f15771,f949]) ).
fof(f15774,plain,
( ron(sK2,sK10(sK3,sK1))
| sK1 = sK3
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ spl54_677 ),
inference(duplicate_literal_removal,[],[f15773]) ).
fof(f15775,plain,
( ron(sK2,sK10(sK3,sK1))
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f15774,f703]) ).
fof(f15776,plain,
( ron(sK2,sK10(sK3,sK1))
| ~ rpoint(sK3)
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f15775,f437]) ).
fof(f15777,plain,
( ron(sK2,sK10(sK3,sK1))
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f15776,f446]) ).
fof(f15787,plain,
( ! [X2,X0,X1] :
( ~ rpoint(sK3)
| rR(sK1,X0,X1)
| rR(sK1,sK2,sK3)
| sK1 = X1
| sK1 = sK3
| sK1 = X0
| sK1 = sK2
| ~ ron(X1,X2)
| ~ ron(X0,X2)
| ~ rpoint(sK1)
| vangle(sK2,sK1,X0) = vangle(sK3,sK1,X1)
| ~ rline(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2) )
| ~ spl54_677 ),
inference(resolution,[],[f15777,f14007]) ).
fof(f16658,plain,
( ! [X0,X1] :
( ~ rpoint(X0)
| vangle(sK3,sK1,X0) = vangle(sK2,sK1,X0)
| ~ rpoint(X0)
| rR(sK1,X0,X0)
| sK1 = X0
| sK1 = X0
| X0 = X1
| ~ rpoint(X1)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) )
| ~ spl54_932 ),
inference(resolution,[],[f15754,f949]) ).
fof(f16659,plain,
( ! [X0,X1] :
( ~ rpoint(X0)
| vangle(sK3,sK1,X0) = vangle(sK2,sK1,X1)
| ~ rpoint(X1)
| rR(sK1,X1,X0)
| sK1 = X1
| sK1 = X0
| X0 = X1
| ~ rpoint(X1)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) )
| ~ spl54_932 ),
inference(resolution,[],[f15754,f951]) ).
fof(f16667,plain,
( ! [X0,X1] :
( rR(sK1,X1,X0)
| vangle(sK3,sK1,X0) = vangle(sK2,sK1,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| sK1 = X1
| sK1 = X0
| X0 = X1 )
| ~ spl54_932 ),
inference(duplicate_literal_removal,[],[f16659]) ).
fof(f16668,plain,
( ! [X0,X1] :
( ~ rpoint(X1)
| vangle(sK3,sK1,X0) = vangle(sK2,sK1,X0)
| rR(sK1,X0,X0)
| sK1 = X0
| X0 = X1
| ~ rpoint(X0) )
| ~ spl54_932 ),
inference(duplicate_literal_removal,[],[f16658]) ).
fof(f16691,plain,
( vangle(sK3,sK1,vd1371) = vangle(sK2,sK1,sK3)
| ~ rpoint(sK3)
| ~ rpoint(vd1371)
| sK1 = sK3
| vd1371 = sK1
| vd1371 = sK3
| rR(sK1,sK3,sK1)
| ~ rpoint(sK1)
| ~ spl54_932 ),
inference(resolution,[],[f16667,f1946]) ).
fof(f16705,plain,
( vangle(sK3,sK1,vd1371) = vangle(sK2,sK1,sK3)
| ~ rpoint(vd1371)
| sK1 = sK3
| vd1371 = sK1
| vd1371 = sK3
| rR(sK1,sK3,sK1)
| ~ rpoint(sK1)
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f16691,f446]) ).
fof(f16717,plain,
( vangle(sK3,sK1,vd1371) = vangle(sK2,sK1,sK3)
| sK1 = sK3
| vd1371 = sK1
| vd1371 = sK3
| rR(sK1,sK3,sK1)
| ~ rpoint(sK1)
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f16705,f436]) ).
fof(f16721,plain,
( vangle(sK3,sK1,vd1371) = vangle(sK2,sK1,sK3)
| vd1371 = sK1
| vd1371 = sK3
| rR(sK1,sK3,sK1)
| ~ rpoint(sK1)
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f16717,f703]) ).
fof(f16724,plain,
( vangle(sK3,sK1,vd1371) = vangle(sK2,sK1,sK3)
| vd1371 = sK3
| rR(sK1,sK3,sK1)
| ~ rpoint(sK1)
| spl54_13
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f16721,f1568]) ).
fof(f16726,plain,
( vangle(sK3,sK1,vd1371) = vangle(sK2,sK1,sK3)
| rR(sK1,sK3,sK1)
| ~ rpoint(sK1)
| spl54_13
| spl54_23
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f16724,f1694]) ).
fof(f16728,plain,
( vangle(sK3,sK1,vd1371) = vangle(sK2,sK1,sK3)
| rR(sK1,sK3,sK1)
| spl54_13
| spl54_23
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f16726,f437]) ).
fof(f16730,plain,
( sF53 = vangle(sK3,sK1,vd1371)
| rR(sK1,sK3,sK1)
| spl54_13
| spl54_23
| ~ spl54_932 ),
inference(forward_demodulation,[],[f16728,f1730]) ).
fof(f16731,plain,
( rR(sK1,sK3,sK1)
| spl54_13
| spl54_23
| spl54_379
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f16730,f7238]) ).
fof(f16735,plain,
( rR(sK1,sK1,sK3)
| ~ rpoint(sK1)
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| spl54_13
| spl54_23
| spl54_379
| ~ spl54_932 ),
inference(resolution,[],[f16731,f889]) ).
fof(f16744,plain,
( rR(sK1,sK1,sK3)
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| spl54_13
| spl54_23
| spl54_379
| ~ spl54_932 ),
inference(duplicate_literal_removal,[],[f16735]) ).
fof(f16749,plain,
( ~ rpoint(sK1)
| ~ rpoint(sK3)
| spl54_13
| spl54_23
| spl54_379
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f16744,f1500]) ).
fof(f16751,plain,
( ~ rpoint(sK3)
| spl54_13
| spl54_23
| spl54_379
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f16749,f437]) ).
fof(f16753,plain,
( $false
| spl54_13
| spl54_23
| spl54_379
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f16751,f446]) ).
fof(f16754,plain,
( spl54_13
| spl54_23
| spl54_379
| ~ spl54_932 ),
inference(avatar_contradiction_clause,[],[f16753]) ).
fof(f16755,plain,
( ! [X2,X0,X1] :
( rR(sK1,X0,X1)
| rR(sK1,sK2,sK3)
| sK1 = X1
| sK1 = sK3
| sK1 = X0
| sK1 = sK2
| ~ ron(X1,X2)
| ~ ron(X0,X2)
| ~ rpoint(sK1)
| vangle(sK2,sK1,X0) = vangle(sK3,sK1,X1)
| ~ rline(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2) )
| ~ spl54_677 ),
inference(forward_subsumption_resolution,[],[f15787,f446]) ).
fof(f16757,plain,
( ! [X2,X0,X1] :
( rR(sK1,X0,X1)
| sK1 = X1
| sK1 = sK3
| sK1 = X0
| sK1 = sK2
| ~ ron(X1,X2)
| ~ ron(X0,X2)
| ~ rpoint(sK1)
| vangle(sK2,sK1,X0) = vangle(sK3,sK1,X1)
| ~ rline(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2) )
| ~ spl54_677
| spl54_931 ),
inference(forward_subsumption_resolution,[],[f16755,f15167]) ).
fof(f16759,plain,
( ! [X2,X0,X1] :
( rR(sK1,X0,X1)
| sK1 = X1
| sK1 = X0
| sK1 = sK2
| ~ ron(X1,X2)
| ~ ron(X0,X2)
| ~ rpoint(sK1)
| vangle(sK2,sK1,X0) = vangle(sK3,sK1,X1)
| ~ rline(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2) )
| ~ spl54_677
| spl54_931 ),
inference(forward_subsumption_resolution,[],[f16757,f703]) ).
fof(f16761,plain,
( ! [X2,X0,X1] :
( rR(sK1,X0,X1)
| sK1 = X1
| sK1 = X0
| ~ ron(X1,X2)
| ~ ron(X0,X2)
| ~ rpoint(sK1)
| vangle(sK2,sK1,X0) = vangle(sK3,sK1,X1)
| ~ rline(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2) )
| ~ spl54_677
| spl54_931 ),
inference(forward_subsumption_resolution,[],[f16759,f701]) ).
fof(f16763,plain,
( ! [X2,X0,X1] :
( rR(sK1,X0,X1)
| sK1 = X1
| sK1 = X0
| ~ ron(X1,X2)
| ~ ron(X0,X2)
| vangle(sK2,sK1,X0) = vangle(sK3,sK1,X1)
| ~ rline(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK2) )
| ~ spl54_677
| spl54_931 ),
inference(forward_subsumption_resolution,[],[f16761,f437]) ).
fof(f16765,plain,
( ! [X2,X0,X1] :
( rR(sK1,X0,X1)
| sK1 = X1
| sK1 = X0
| ~ ron(X1,X2)
| ~ ron(X0,X2)
| vangle(sK2,sK1,X0) = vangle(sK3,sK1,X1)
| ~ rline(X2)
| ~ rpoint(X1)
| ~ rpoint(X0) )
| ~ spl54_677
| spl54_931 ),
inference(forward_subsumption_resolution,[],[f16763,f444]) ).
fof(f16767,plain,
( spl54_932
| ~ spl54_677
| spl54_931 ),
inference(avatar_split_clause,[],[f16765,f15166,f11965,f15170]) ).
fof(f16775,plain,
( vd684 = vangle(sK3,sK1,vd1371)
| ~ spl54_379
| ~ spl54_677 ),
inference(forward_demodulation,[],[f7239,f11967]) ).
fof(f16945,plain,
( ! [X0] :
( vangle(sK3,sK1,X0) = vangle(sK2,sK1,X0)
| rR(sK1,X0,X0)
| sK1 = X0
| sK1 = X0
| ~ rpoint(X0) )
| ~ spl54_932 ),
inference(resolution,[],[f16668,f437]) ).
fof(f16948,plain,
( ! [X0] :
( rR(sK1,X0,X0)
| vangle(sK3,sK1,X0) = vangle(sK2,sK1,X0)
| sK1 = X0
| ~ rpoint(X0) )
| ~ spl54_932 ),
inference(duplicate_literal_removal,[],[f16945]) ).
fof(f16960,plain,
( ! [X0] :
( vangle(sK3,sK1,X0) = vangle(sK2,sK1,X0)
| sK1 = X0
| ~ rpoint(X0)
| ~ rpoint(X0)
| ~ rpoint(sK1) )
| ~ spl54_932 ),
inference(resolution,[],[f16948,f1501]) ).
fof(f16961,plain,
( ! [X0] :
( vangle(sK3,sK1,X0) = vangle(sK2,sK1,X0)
| sK1 = X0
| ~ rpoint(X0)
| ~ rpoint(sK1) )
| ~ spl54_932 ),
inference(duplicate_literal_removal,[],[f16960]) ).
fof(f16973,plain,
( ! [X0] :
( ~ rpoint(X0)
| sK1 = X0
| vangle(sK3,sK1,X0) = vangle(sK2,sK1,X0) )
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f16961,f437]) ).
fof(f17003,plain,
( vd1371 = sK1
| vangle(sK3,sK1,vd1371) = vangle(sK2,sK1,vd1371)
| ~ spl54_932 ),
inference(resolution,[],[f16973,f436]) ).
fof(f17026,plain,
( vangle(sK3,sK1,vd1371) = vangle(sK2,sK1,vd1371)
| spl54_13
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f17003,f1568]) ).
fof(f17029,plain,
( sF52 = vangle(sK3,sK1,vd1371)
| spl54_13
| spl54_26
| ~ spl54_932 ),
inference(forward_demodulation,[],[f17026,f4086]) ).
fof(f17032,plain,
( vd684 = sF52
| spl54_13
| spl54_26
| ~ spl54_379
| ~ spl54_677
| ~ spl54_932 ),
inference(forward_demodulation,[],[f17029,f16775]) ).
fof(f17033,plain,
( $false
| spl54_13
| spl54_26
| ~ spl54_379
| ~ spl54_677
| spl54_881
| ~ spl54_932 ),
inference(forward_subsumption_resolution,[],[f17032,f13869]) ).
fof(f17034,plain,
( spl54_13
| spl54_26
| ~ spl54_379
| ~ spl54_677
| spl54_881
| ~ spl54_932 ),
inference(avatar_contradiction_clause,[],[f17033]) ).
fof(f17036,plain,
( $false
| ~ spl54_677
| ~ spl54_881 ),
inference(forward_subsumption_resolution,[],[f15755,f13868]) ).
fof(f17037,plain,
( ~ spl54_677
| ~ spl54_881 ),
inference(avatar_contradiction_clause,[],[f17036]) ).
fof(f17062,plain,
( spl54_881
| ~ spl54_26 ),
inference(avatar_split_clause,[],[f1810,f1779,f13867]) ).
fof(f17107,plain,
( $false
| spl54_677
| spl54_933 ),
inference(forward_subsumption_resolution,[],[f15662,f11966]) ).
fof(f17108,plain,
( spl54_677
| spl54_933 ),
inference(avatar_contradiction_clause,[],[f17107]) ).
cnf(s21,plain,
( ~ spl54_13
| spl54_14 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s22,plain,
~ spl54_14,
inference(sat_conversion,[],[f1643]) ).
cnf(s28,plain,
~ spl54_23,
inference(sat_conversion,[],[f1722]) ).
cnf(s828,plain,
( ~ spl54_677
| spl54_913
| ~ spl54_914 ),
inference(sat_conversion,[],[f14387]) ).
cnf(s851,plain,
( spl54_914
| ~ spl54_931 ),
inference(sat_conversion,[],[f15220]) ).
cnf(s852,plain,
( ~ spl54_931
| ~ spl54_933 ),
inference(sat_conversion,[],[f15222]) ).
cnf(s854,plain,
( spl54_677
| spl54_931 ),
inference(sat_conversion,[],[f15283]) ).
cnf(s856,plain,
~ spl54_913,
inference(sat_conversion,[],[f15453]) ).
cnf(s889,plain,
( spl54_13
| spl54_23
| spl54_379
| ~ spl54_932 ),
inference(sat_conversion,[],[f16754]) ).
cnf(s890,plain,
( ~ spl54_677
| spl54_931
| spl54_932 ),
inference(sat_conversion,[],[f16767]) ).
cnf(s893,plain,
( spl54_13
| spl54_26
| ~ spl54_379
| ~ spl54_677
| spl54_881
| ~ spl54_932 ),
inference(sat_conversion,[],[f17034]) ).
cnf(s894,plain,
( ~ spl54_677
| ~ spl54_881 ),
inference(sat_conversion,[],[f17037]) ).
cnf(s897,plain,
( ~ spl54_26
| spl54_881 ),
inference(sat_conversion,[],[f17062]) ).
cnf(s907,plain,
( spl54_677
| spl54_933 ),
inference(sat_conversion,[],[f17108]) ).
cnf(s927,plain,
( ~ spl54_677
| ~ spl54_914 ),
inference(rat,[],[s828,s856]) ).
cnf(s1018,plain,
~ spl54_13,
inference(rat,[],[s21,s22]) ).
cnf(s1038,plain,
spl54_677,
inference(rat,[],[s852,s854,s907]) ).
cnf(s1039,plain,
~ spl54_881,
inference(rat,[],[s894,s1038]) ).
cnf(s1046,plain,
~ spl54_914,
inference(rat,[],[s927,s1038]) ).
cnf(s1048,plain,
~ spl54_26,
inference(rat,[],[s897,s1039]) ).
cnf(s1049,plain,
~ spl54_931,
inference(rat,[],[s851,s1046]) ).
cnf(s1052,plain,
spl54_932,
inference(rat,[],[s890,s1038,s1049]) ).
cnf(s1053,plain,
spl54_379,
inference(rat,[],[s889,s1018,s28,s1052]) ).
cnf(s1054,plain,
$false,
inference(rat,[],[s893,s1048,s1039,s1038,s1018,s1052,s1053]) ).
fof(f17184,plain,
$false,
inference(avatar_sat_refutation,[],[s1054]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO333+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 08:06:30 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.80/2.71 % (1710224)Detected formulas, will run a generic FOF schedule.
% 12.80/2.71 % (1710235)dis-21_1_sil=8000:lcm=predicate:random_seed=4021112217: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.80/2.71 % (1710235)Instruction limit reached!
% 12.80/2.71 % (1710235)------------------------------
% 12.80/2.71 % (1710235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.71 % (1710235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.71 % (1710235)CaDiCaL version: 2.1.3
% 12.80/2.71 % (1710235)Termination reason: Instruction limit
% 12.80/2.71 % (1710235)Termination phase: Saturation
% 12.80/2.71 % (1710235)Time elapsed: 0.031 s
% 12.80/2.71 % (1710235)Peak memory usage: 89 MB
% 12.80/2.71 % (1710235)Instructions burned: 134 (million)
% 12.80/2.71 % (1710229)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=4017386753:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.80/2.71 % (1710233)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1619399966:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.80/2.71 % (1710232)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=789956:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.80/2.71 % (1710230)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=3253182860:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.80/2.71 % (1710231)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=3908835050:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.80/2.71 % (1710234)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1038727259:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.80/2.71 % (1710232)Instruction limit reached!
% 12.80/2.71 % (1710232)------------------------------
% 12.80/2.71 % (1710232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.71 % (1710232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.71 % (1710232)CaDiCaL version: 2.1.3
% 12.80/2.71 % (1710232)Termination reason: Instruction limit
% 12.80/2.71 % (1710232)Termination phase: Saturation
% 12.80/2.71 % (1710232)Time elapsed: 0.058 s
% 12.80/2.71 % (1710232)Peak memory usage: 90 MB
% 12.80/2.71 % (1710232)Instructions burned: 110 (million)
% 12.80/2.71 % (1710233)Instruction limit reached!
% 12.80/2.71 % (1710233)------------------------------
% 12.80/2.71 % (1710233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.71 % (1710233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.71 % (1710233)CaDiCaL version: 2.1.3
% 12.80/2.71 % (1710233)Termination reason: Instruction limit
% 12.80/2.71 % (1710233)Termination phase: Saturation
% 12.80/2.71 % (1710233)Time elapsed: 0.061 s
% 12.80/2.71 % (1710233)Peak memory usage: 89 MB
% 12.80/2.71 % (1710233)Instructions burned: 120 (million)
% 12.80/2.71 % (1710237)lrs+10_1_sil=8000:sp=occurrence:random_seed=1387341440:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 12.80/2.71 % (1710234)Instruction limit reached!
% 12.80/2.71 % (1710234)------------------------------
% 12.80/2.71 % (1710234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.71 % (1710234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.71 % (1710234)CaDiCaL version: 2.1.3
% 12.80/2.71 % (1710234)Termination reason: Instruction limit
% 12.80/2.71 % (1710234)Termination phase: Saturation
% 12.80/2.71 % (1710234)Time elapsed: 0.081 s
% 12.80/2.71 % (1710234)Peak memory usage: 90 MB
% 12.80/2.71 % (1710234)Instructions burned: 139 (million)
% 12.80/2.71 % (1710237)Instruction limit reached!
% 12.80/2.71 % (1710237)------------------------------
% 12.80/2.71 % (1710237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.71 % (1710237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.71 % (1710237)CaDiCaL version: 2.1.3
% 12.80/2.71 % (1710237)Termination reason: Instruction limit
% 12.80/2.71 % (1710237)Termination phase: Saturation
% 12.80/2.71 % (1710237)Time elapsed: 0.086 s
% 12.80/2.71 % (1710237)Peak memory usage: 93 MB
% 12.80/2.71 % (1710237)Instructions burned: 288 (million)
% 16.92/3.22 % (1710244)lrs+10_1_sil=32000:urr=on:br=off:random_seed=765645787:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 16.92/3.22 % (1710245)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3936834986:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 16.92/3.22 % (1710247)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=2438701070:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 16.92/3.22 % (1710248)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1152629177:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 16.92/3.22 % (1710244)Instruction limit reached!
% 16.92/3.22 % (1710244)------------------------------
% 16.92/3.22 % (1710244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.92/3.22 % (1710244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.92/3.22 % (1710244)CaDiCaL version: 2.1.3
% 16.92/3.22 % (1710244)Termination reason: Instruction limit
% 16.92/3.22 % (1710244)Termination phase: Saturation
% 16.92/3.22 % (1710244)Time elapsed: 0.076 s
% 16.92/3.22 % (1710244)Peak memory usage: 91 MB
% 16.92/3.22 % (1710244)Instructions burned: 157 (million)
% 16.92/3.22 % (1710247)Instruction limit reached!
% 16.92/3.22 % (1710247)------------------------------
% 16.92/3.22 % (1710247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.92/3.22 % (1710247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.92/3.22 % (1710247)CaDiCaL version: 2.1.3
% 16.92/3.22 % (1710247)Termination reason: Instruction limit
% 16.92/3.22 % (1710247)Termination phase: Saturation
% 16.92/3.22 % (1710247)Time elapsed: 0.116 s
% 16.92/3.22 % (1710247)Peak memory usage: 93 MB
% 16.92/3.22 % (1710247)Instructions burned: 249 (million)
% 16.92/3.22 % (1710248)Instruction limit reached!
% 16.92/3.22 % (1710248)------------------------------
% 16.92/3.22 % (1710248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.92/3.22 % (1710248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.92/3.22 % (1710248)CaDiCaL version: 2.1.3
% 16.92/3.22 % (1710248)Termination reason: Instruction limit
% 16.92/3.22 % (1710248)Termination phase: Saturation
% 16.92/3.22 % (1710248)Time elapsed: 0.078 s
% 16.92/3.22 % (1710248)Peak memory usage: 89 MB
% 16.92/3.22 % (1710248)Instructions burned: 297 (million)
% 16.92/3.22 % (1710245)Instruction limit reached!
% 16.92/3.22 % (1710245)------------------------------
% 16.92/3.22 % (1710245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.92/3.22 % (1710245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.92/3.22 % (1710245)CaDiCaL version: 2.1.3
% 16.92/3.22 % (1710245)Termination reason: Instruction limit
% 16.92/3.22 % (1710245)Termination phase: Saturation
% 16.92/3.22 % (1710245)Time elapsed: 0.179 s
% 16.92/3.22 % (1710245)Peak memory usage: 91 MB
% 16.92/3.22 % (1710245)Instructions burned: 326 (million)
% 16.92/3.22 % (1710253)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3056388894:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 16.92/3.22 % (1710255)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1527215777:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 16.92/3.22 % (1710255)Refutation not found, incomplete strategy
% 16.92/3.22 % (1710255)------------------------------
% 16.92/3.22 % (1710255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.92/3.22 % (1710255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.92/3.22 % (1710255)CaDiCaL version: 2.1.3
% 16.92/3.22 % (1710255)Termination reason: Refutation not found, incomplete strategy
% 16.92/3.22 % (1710255)Time elapsed: 0.014 s
% 16.92/3.22 % (1710255)Peak memory usage: 89 MB
% 16.92/3.22 % (1710255)Instructions burned: 51 (million)
% 16.92/3.22 % (1710254)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4112320806:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 16.92/3.22 % (1710254)Instruction limit reached!
% 16.92/3.22 % (1710254)------------------------------
% 16.92/3.22 % (1710254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.92/3.22 % (1710254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.92/3.22 % (1710254)CaDiCaL version: 2.1.3
% 16.92/3.22 % (1710254)Termination reason: Instruction limit
% 16.92/3.22 % (1710254)Termination phase: Saturation
% 15.10/3.32 % (1710254)Time elapsed: 0.059 s
% 15.10/3.32 % (1710254)Peak memory usage: 90 MB
% 15.10/3.32 % (1710254)Instructions burned: 115 (million)
% 15.10/3.32 % (1710256)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=839632049:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 15.10/3.32 % (1710256)Instruction limit reached!
% 15.10/3.32 % (1710256)------------------------------
% 15.10/3.32 % (1710256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.32 % (1710256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.32 % (1710256)CaDiCaL version: 2.1.3
% 15.10/3.32 % (1710256)Termination reason: Instruction limit
% 15.10/3.32 % (1710256)Termination phase: Saturation
% 15.10/3.32 % (1710256)Time elapsed: 0.047 s
% 15.10/3.32 % (1710256)Peak memory usage: 89 MB
% 15.10/3.32 % (1710256)Instructions burned: 117 (million)
% 15.10/3.32 % (1710255)------------------------------
% 15.10/3.32 % (1710255)------------------------------
% 15.10/3.32 % (1710261)lrs+10_1_sil=8000:sp=occurrence:random_seed=3540154937:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 15.10/3.32 % (1710263)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2823137891:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 15.10/3.32 % (1710262)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=915167146:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 15.10/3.32 % (1710262)Refutation not found, incomplete strategy
% 15.10/3.32 % (1710262)------------------------------
% 15.10/3.32 % (1710262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.32 % (1710262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.32 % (1710262)CaDiCaL version: 2.1.3
% 15.10/3.32 % (1710262)Termination reason: Refutation not found, incomplete strategy
% 15.10/3.32 % (1710262)Time elapsed: 0.018 s
% 15.10/3.32 % (1710262)Peak memory usage: 90 MB
% 15.10/3.32 % (1710262)Instructions burned: 32 (million)
% 15.10/3.32 % (1710262)------------------------------
% 15.10/3.32 % (1710262)------------------------------
% 15.10/3.32 % (1710267)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2089409053:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 15.10/3.32 % (1710261)Instruction limit reached!
% 15.10/3.32 % (1710261)------------------------------
% 15.10/3.32 % (1710261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.32 % (1710261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.32 % (1710261)CaDiCaL version: 2.1.3
% 15.10/3.32 % (1710261)Termination reason: Instruction limit
% 15.10/3.32 % (1710261)Termination phase: Saturation
% 15.10/3.32 % (1710261)Time elapsed: 0.498 s
% 15.10/3.32 % (1710261)Peak memory usage: 99 MB
% 15.10/3.32 % (1710261)Instructions burned: 908 (million)
% 15.10/3.32 % (1710267)Instruction limit reached!
% 15.10/3.32 % (1710267)------------------------------
% 15.10/3.32 % (1710267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.32 % (1710267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.32 % (1710267)CaDiCaL version: 2.1.3
% 15.10/3.32 % (1710267)Termination reason: Instruction limit
% 15.10/3.32 % (1710267)Termination phase: Saturation
% 15.10/3.32 % (1710267)Time elapsed: 0.063 s
% 15.10/3.32 % (1710267)Peak memory usage: 92 MB
% 15.10/3.32 % (1710267)Instructions burned: 136 (million)
% 15.10/3.32 % (1710270)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=805257069:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 15.10/3.32 % (1710269)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4006396263:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 15.10/3.32 % (1710269)Instruction limit reached!
% 15.10/3.32 % (1710269)------------------------------
% 15.10/3.32 % (1710269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.32 % (1710269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.32 % (1710269)CaDiCaL version: 2.1.3
% 15.10/3.32 % (1710269)Termination reason: Instruction limit
% 15.10/3.32 % (1710269)Termination phase: Saturation
% 15.10/3.32 % (1710269)Time elapsed: 0.314 s
% 15.10/3.32 % (1710269)Peak memory usage: 95 MB
% 15.10/3.32 % (1710269)Instructions burned: 592 (million)
% 15.10/3.32 % (1710273)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=2341798021:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 15.10/3.32 % (1710273)Instruction limit reached!
% 15.10/3.32 % (1710273)------------------------------
% 15.10/3.32 % (1710273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.32 % (1710273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.32 % (1710273)CaDiCaL version: 2.1.3
% 15.10/3.32 % (1710273)Termination reason: Instruction limit
% 15.10/3.32 % (1710273)Termination phase: Saturation
% 15.10/3.32 % (1710273)Time elapsed: 0.063 s
% 15.10/3.32 % (1710273)Peak memory usage: 89 MB
% 15.10/3.32 % (1710273)Instructions burned: 126 (million)
% 15.10/3.32 % (1710253)Instruction limit reached!
% 15.10/3.32 % (1710253)------------------------------
% 15.10/3.32 % (1710253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.32 % (1710253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.32 % (1710253)CaDiCaL version: 2.1.3
% 15.10/3.32 % (1710253)Termination reason: Instruction limit
% 15.10/3.32 % (1710253)Termination phase: Saturation
% 15.10/3.32 % (1710253)Time elapsed: 1.454 s
% 15.10/3.32 % (1710253)Peak memory usage: 140 MB
% 15.10/3.32 % (1710253)Instructions burned: 2351 (million)
% 15.10/3.32 % (1710275)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3662586623:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 15.10/3.32 % (1710275)Instruction limit reached!
% 15.10/3.32 % (1710275)------------------------------
% 15.10/3.32 % (1710275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.32 % (1710275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.32 % (1710275)CaDiCaL version: 2.1.3
% 15.10/3.32 % (1710275)Termination reason: Instruction limit
% 15.10/3.32 % (1710275)Termination phase: Saturation
% 15.10/3.32 % (1710275)Time elapsed: 0.075 s
% 15.10/3.32 % (1710275)Peak memory usage: 91 MB
% 15.10/3.32 % (1710275)Instructions burned: 134 (million)
% 15.10/3.32 % (1710276)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=256885563:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 15.10/3.32 % (1710276)Refutation not found, incomplete strategy
% 15.10/3.32 % (1710276)------------------------------
% 15.10/3.32 % (1710276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.32 % (1710276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.32 % (1710276)CaDiCaL version: 2.1.3
% 15.10/3.32 % (1710276)Termination reason: Refutation not found, incomplete strategy
% 15.10/3.32 % (1710276)Time elapsed: 0.014 s
% 15.10/3.32 % (1710276)Peak memory usage: 89 MB
% 15.10/3.32 % (1710276)Instructions burned: 26 (million)
% 15.10/3.32 % (1710229)First to succeed.
% 15.10/3.32 % (1710229)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1710224"
% 15.10/3.32 % (1710278)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3453572242:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi)
% 15.10/3.32 % (1710263)Instruction limit reached!
% 15.10/3.32 % (1710263)------------------------------
% 15.10/3.32 % (1710263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.32 % (1710263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.32 % (1710263)CaDiCaL version: 2.1.3
% 15.10/3.32 % (1710263)Termination reason: Instruction limit
% 15.10/3.32 % (1710263)Termination phase: Saturation
% 15.10/3.32 % (1710263)Time elapsed: 1.460 s
% 15.10/3.32 % (1710263)Peak memory usage: 145 MB
% 15.10/3.32 % (1710263)Instructions burned: 5206 (million)
% 15.10/3.32 % (1710278)Refutation not found, incomplete strategy
% 15.10/3.32 % (1710278)------------------------------
% 15.10/3.32 % (1710278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.32 % (1710278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.32 % (1710278)CaDiCaL version: 2.1.3
% 15.10/3.32 % (1710278)Termination reason: Refutation not found, incomplete strategy
% 15.10/3.32 % (1710278)Time elapsed: 0.007 s
% 15.10/3.32 % (1710278)Peak memory usage: 89 MB
% 15.10/3.32 % (1710278)Instructions burned: 11 (million)
% 15.10/3.32 % (1710281)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=2677629434:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi)
% 15.10/3.32 % (1710276)------------------------------
% 15.10/3.32 % (1710276)------------------------------
% 15.10/3.32 % (1710229)Refutation found. Thanks to Tanya!
% 15.10/3.32 % SZS status Theorem for theBenchmark
% 15.10/3.32 % SZS output start Proof for theBenchmark
% See solution above
% 18.09/3.52 % (1710229)------------------------------
% 18.09/3.52 % (1710229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.09/3.52 % (1710229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.09/3.52 % (1710229)CaDiCaL version: 2.1.3
% 18.09/3.52 % (1710229)Termination reason: Refutation
% 18.09/3.52 % (1710229)Time elapsed: 2.047 s
% 18.09/3.52 % (1710229)Peak memory usage: 148 MB
% 18.09/3.52 % (1710229)Instructions burned: 3465 (million)
% 18.09/3.52 % (1710229)------------------------------
% 18.09/3.52 % (1710229)------------------------------
% 18.09/3.52 % (1710224)Success in time 2.475 s
% 18.09/3.52 % Vampire exiting
%------------------------------------------------------------------------------