%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO334+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:52:29 AM UTC 2026
% Result : Theorem 20.48s 3.70s
% Output : Refutation 20.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 56
% Syntax : Number of formulae : 716 ( 86 unt; 30 def)
% Number of atoms : 4759 (1792 equ)
% Maximal formula atoms : 26 ( 6 avg)
% Number of connectives : 6961 (2918 ~;3827 |; 172 &)
% ( 31 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 9 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 29 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 11 con; 0-3 aty)
% Number of variables : 1476 ( 0 sgn1420 !; 56 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vf(vd1371,vd1363) = vf(vd1361,vd1362),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(392, 1376, 0)') ).
fof(f2,negated_conjecture,
vf(vd1371,vd1363) != vf(vd1361,vd1362),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
vangle(vd1371,vd1362,vd1363) = vangle(vd1361,vd1363,vd1362),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(391), 1375, 0)') ).
fof(f5,axiom,
vf(vd1362,vd1371) = vf(vd1361,vd1363),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(390), 1373, 0)') ).
fof(f6,axiom,
rR(vd1371,vd1362,vd1361),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(390), 1372, 0)') ).
fof(f7,axiom,
rpoint(vd1371),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(390, 0)') ).
fof(f8,axiom,
? [X0] :
( vd1362 = X0
& rpoint(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(s2(plural(386)))') ).
fof(f9,axiom,
! [X0,X1] :
( ( ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> vf(X0,X1) = vf(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(166), 0), imp(cond(axiom(166), 0)))') ).
fof(f12,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( ~ ? [X6] :
( ron(X5,X6)
& ron(X4,X6)
& ron(X3,X6)
& rline(X6) )
& vangle(X1,X0,X2) = vangle(X4,X3,X5)
& vf(X0,X2) = vf(X3,X5)
& vf(X0,X1) = vf(X3,X4)
& ? [X7] :
( X5 = X7
& rpoint(X7) )
& ? [X8] :
( X4 = X8
& rpoint(X8) )
& ? [X9] :
( X3 = X9
& rpoint(X9) )
& X1 != X2
& X0 != X2
& X0 != X1
& ? [X10] :
( X2 = X10
& rpoint(X10) )
& ? [X11] :
( X1 = X11
& rpoint(X11) )
& ? [X12] :
( X0 = X12
& rpoint(X12) ) )
=> vf(X1,X2) = vf(X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(264), 0), 2)') ).
fof(f15,axiom,
vangle(vd1361,vd1362,vd1363) = vangle(vd1361,vd1363,vd1362),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(386, 1365, 0)') ).
fof(f16,axiom,
vd1362 != vd1363,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(386, 9)') ).
fof(f17,axiom,
vd1361 != vd1363,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(386, 8)') ).
fof(f18,axiom,
vd1361 != vd1362,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(386, 7)') ).
fof(f19,axiom,
? [X0] :
( vd1363 = X0
& rpoint(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(s3(plural(386)))') ).
fof(f20,axiom,
? [X0] :
( vd1361 = X0
& rpoint(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(s1(plural(386)))') ).
fof(f29,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ron(X2,X6)
& ron(X0,X6)
& X0 != X4
& X0 != X2
& X6 = X7
& rline(X7)
& X4 = X5
& rpoint(X5)
& X2 = X3
& rpoint(X3)
& X0 = X1
& rpoint(X1) )
=> ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
<=> vangle(X2,X0,X4) = v0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(188), 0), imp(cond(axiom(188), 0)))') ).
fof(f33,axiom,
! [X0,X1] :
( ( ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ? [X4] :
( vf(X0,X1) = X4
& rreal(X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(160), 0), imp(cond(axiom(160), 0)))') ).
fof(f37,axiom,
! [X0,X1,X2,X3,X4] :
( ( X3 = X4
& ron(X2,X3)
& ron(X1,X3)
& ron(X0,X3)
& rline(X4)
& X1 != X2
& X0 != X2
& X0 != X1
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(91), 0), imp(cond(axiom(91), 0)))') ).
fof(f40,axiom,
! [X0,X1,X2] :
( ( rR(X1,X0,X2)
& ? [X3] :
( X2 = X3
& rpoint(X3) )
& ? [X4] :
( X1 = X4
& rpoint(X4) )
& ? [X5] :
( X0 = X5
& rpoint(X5) ) )
=> ( ~ rR(X0,X1,X2)
& X0 != X2
& X0 != X1
& rR(X1,X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))') ).
fof(f45,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(f50,axiom,
v0 = vd684,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(axiom(137), 2)') ).
fof(f53,axiom,
! [X0,X1,X2,X3,X4] :
( ( X3 = X4
& ron(X1,X3)
& ron(X0,X3)
& rR(X1,X0,X2)
& rline(X4)
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ron(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(83), 0), imp(cond(axiom(83), 0)))') ).
fof(f55,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(f56,axiom,
! [X0,X1,X2] :
( ( rR(X1,X0,X2)
& ? [X3] :
( X2 = X3
& rpoint(X3) )
& ? [X4] :
( X1 = X4
& rpoint(X4) )
& ? [X5] :
( X0 = X5
& rpoint(X5) ) )
=> vplus(vf(X0,X1),vf(X1,X2)) = vf(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(180), 0), imp(cond(axiom(180), 0)))') ).
fof(f58,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(f84,axiom,
! [X0,X1,X2,X3] :
( ( rR(X1,X0,X3)
& rR(X1,X0,X2)
& ? [X4] :
( X3 = X4
& rpoint(X4) )
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ~ rR(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(93), 0), imp(cond(axiom(93), 0)))') ).
fof(f85,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(f132,plain,
vf(vd1371,vd1363) != vf(vd1361,vd1362),
inference(flattening,[],[f2]) ).
fof(f137,plain,
! [X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f9]) ).
fof(f138,plain,
! [X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f137]) ).
fof(f143,plain,
! [X0,X1,X2,X3,X4,X5] :
( vf(X1,X2) = vf(X4,X5)
| ? [X6] :
( ron(X5,X6)
& ron(X4,X6)
& ron(X3,X6)
& rline(X6) )
| vangle(X1,X0,X2) != vangle(X4,X3,X5)
| vf(X0,X2) != vf(X3,X5)
| vf(X0,X1) != vf(X3,X4)
| ! [X7] :
( X5 != X7
| ~ rpoint(X7) )
| ! [X8] :
( X4 != X8
| ~ rpoint(X8) )
| ! [X9] :
( X3 != X9
| ~ rpoint(X9) )
| X1 = X2
| X0 = X2
| X0 = X1
| ! [X10] :
( X2 != X10
| ~ rpoint(X10) )
| ! [X11] :
( X1 != X11
| ~ rpoint(X11) )
| ! [X12] :
( X0 != X12
| ~ rpoint(X12) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f144,plain,
! [X0,X1,X2,X3,X4,X5] :
( vf(X1,X2) = vf(X4,X5)
| ? [X6] :
( ron(X5,X6)
& ron(X4,X6)
& ron(X3,X6)
& rline(X6) )
| vangle(X1,X0,X2) != vangle(X4,X3,X5)
| vf(X0,X2) != vf(X3,X5)
| vf(X0,X1) != vf(X3,X4)
| ! [X7] :
( X5 != X7
| ~ rpoint(X7) )
| ! [X8] :
( X4 != X8
| ~ rpoint(X8) )
| ! [X9] :
( X3 != X9
| ~ rpoint(X9) )
| X1 = X2
| X0 = X2
| X0 = X1
| ! [X10] :
( X2 != X10
| ~ rpoint(X10) )
| ! [X11] :
( X1 != X11
| ~ rpoint(X11) )
| ! [X12] :
( X0 != X12
| ~ rpoint(X12) ) ),
inference(flattening,[],[f143]) ).
fof(f161,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,[],[f29]) ).
fof(f162,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,[],[f161]) ).
fof(f169,plain,
! [X0,X1] :
( ? [X4] :
( vf(X0,X1) = X4
& rreal(X4) )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f33]) ).
fof(f170,plain,
! [X0,X1] :
( ? [X4] :
( vf(X0,X1) = X4
& rreal(X4) )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f169]) ).
fof(f177,plain,
! [X0,X1,X2,X3,X4] :
( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f37]) ).
fof(f178,plain,
! [X0,X1,X2,X3,X4] :
( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f177]) ).
fof(f183,plain,
! [X0,X1,X2] :
( ( ~ rR(X0,X1,X2)
& X0 != X2
& X0 != X1
& rR(X1,X2,X0) )
| ~ rR(X1,X0,X2)
| ! [X3] :
( X2 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(ennf_transformation,[],[f40]) ).
fof(f184,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,[],[f183]) ).
fof(f193,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,[],[f45]) ).
fof(f194,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,[],[f193]) ).
fof(f203,plain,
! [X0,X1,X2,X3,X4] :
( ron(X2,X3)
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f53]) ).
fof(f204,plain,
! [X0,X1,X2,X3,X4] :
( ron(X2,X3)
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f203]) ).
fof(f207,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,[],[f55]) ).
fof(f208,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,[],[f207]) ).
fof(f209,plain,
! [X0,X1,X2] :
( vplus(vf(X0,X1),vf(X1,X2)) = vf(X0,X2)
| ~ rR(X1,X0,X2)
| ! [X3] :
( X2 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(ennf_transformation,[],[f56]) ).
fof(f210,plain,
! [X0,X1,X2] :
( vplus(vf(X0,X1),vf(X1,X2)) = vf(X0,X2)
| ~ rR(X1,X0,X2)
| ! [X3] :
( X2 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(flattening,[],[f209]) ).
fof(f213,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,[],[f58]) ).
fof(f214,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,[],[f213]) ).
fof(f264,plain,
! [X0,X1,X2,X3] :
( ~ rR(X1,X2,X3)
| ~ rR(X1,X0,X3)
| ~ rR(X1,X0,X2)
| ! [X4] :
( X3 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f84]) ).
fof(f265,plain,
! [X0,X1,X2,X3] :
( ~ rR(X1,X2,X3)
| ~ rR(X1,X0,X3)
| ~ rR(X1,X0,X2)
| ! [X4] :
( X3 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f264]) ).
fof(f266,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,[],[f85]) ).
fof(f267,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,[],[f266]) ).
fof(f353,plain,
( vd1362 = sK1
& rpoint(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X0,sK1)],[f8]) ).
fof(f356,plain,
! [X0,X1,X2,X3,X4,X5] :
( vf(X1,X2) = vf(X4,X5)
| ( ron(X5,sK4(X3,X4,X5))
& ron(X4,sK4(X3,X4,X5))
& ron(X3,sK4(X3,X4,X5))
& rline(sK4(X3,X4,X5)) )
| vangle(X1,X0,X2) != vangle(X4,X3,X5)
| vf(X0,X2) != vf(X3,X5)
| vf(X0,X1) != vf(X3,X4)
| ! [X7] :
( X5 != X7
| ~ rpoint(X7) )
| ! [X8] :
( X4 != X8
| ~ rpoint(X8) )
| ! [X9] :
( X3 != X9
| ~ rpoint(X9) )
| X1 = X2
| X0 = X2
| X0 = X1
| ! [X10] :
( X2 != X10
| ~ rpoint(X10) )
| ! [X11] :
( X1 != X11
| ~ rpoint(X11) )
| ! [X12] :
( X0 != X12
| ~ rpoint(X12) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X6,sK4(X3,X4,X5))],[f144]) ).
fof(f357,plain,
( vd1363 = sK5
& rpoint(sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X0,sK5)],[f19]) ).
fof(f358,plain,
( vd1361 = sK6
& rpoint(sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X0,sK6)],[f20]) ).
fof(f365,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,[],[f162]) ).
fof(f366,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,[],[f365]) ).
fof(f370,plain,
! [X0,X1] :
( ? [X2] :
( vf(X0,X1) = X2
& rreal(X2) )
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(rectify,[],[f170]) ).
fof(f371,plain,
! [X0,X1] :
( ( vf(X0,X1) = sK7(X0,X1)
& rreal(sK7(X0,X1)) )
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f370]) ).
fof(f375,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,[],[f214]) ).
fof(f376,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))],[f375]) ).
fof(f433,plain,
vf(vd1371,vd1363) != vf(vd1361,vd1362),
inference(cnf_transformation,[],[f132]) ).
fof(f434,plain,
vangle(vd1371,vd1362,vd1363) = vangle(vd1361,vd1363,vd1362),
inference(cnf_transformation,[],[f3]) ).
fof(f436,plain,
vf(vd1361,vd1363) = vf(vd1362,vd1371),
inference(cnf_transformation,[],[f5]) ).
fof(f437,plain,
rR(vd1371,vd1362,vd1361),
inference(cnf_transformation,[],[f6]) ).
fof(f438,plain,
rpoint(vd1371),
inference(cnf_transformation,[],[f7]) ).
fof(f439,plain,
rpoint(sK1),
inference(cnf_transformation,[],[f353]) ).
fof(f440,plain,
vd1362 = sK1,
inference(cnf_transformation,[],[f353]) ).
fof(f441,plain,
! [X2,X3,X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| X1 != X2
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(cnf_transformation,[],[f138]) ).
fof(f450,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X5,X12] :
( vf(X1,X2) = vf(X4,X5)
| rline(sK4(X3,X4,X5))
| vangle(X1,X0,X2) != vangle(X4,X3,X5)
| vf(X0,X2) != vf(X3,X5)
| vf(X0,X1) != vf(X3,X4)
| X5 != X7
| ~ rpoint(X7)
| X4 != X8
| ~ rpoint(X8)
| X3 != X9
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(cnf_transformation,[],[f356]) ).
fof(f451,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X5,X12] :
( vf(X1,X2) = vf(X4,X5)
| ron(X3,sK4(X3,X4,X5))
| vangle(X1,X0,X2) != vangle(X4,X3,X5)
| vf(X0,X2) != vf(X3,X5)
| vf(X0,X1) != vf(X3,X4)
| X5 != X7
| ~ rpoint(X7)
| X4 != X8
| ~ rpoint(X8)
| X3 != X9
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(cnf_transformation,[],[f356]) ).
fof(f452,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X5,X12] :
( vf(X1,X2) = vf(X4,X5)
| ron(X4,sK4(X3,X4,X5))
| vangle(X1,X0,X2) != vangle(X4,X3,X5)
| vf(X0,X2) != vf(X3,X5)
| vf(X0,X1) != vf(X3,X4)
| X5 != X7
| ~ rpoint(X7)
| X4 != X8
| ~ rpoint(X8)
| X3 != X9
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(cnf_transformation,[],[f356]) ).
fof(f453,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X5,X12] :
( vf(X1,X2) = vf(X4,X5)
| ron(X5,sK4(X3,X4,X5))
| vangle(X1,X0,X2) != vangle(X4,X3,X5)
| vf(X0,X2) != vf(X3,X5)
| vf(X0,X1) != vf(X3,X4)
| X5 != X7
| ~ rpoint(X7)
| X4 != X8
| ~ rpoint(X8)
| X3 != X9
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(cnf_transformation,[],[f356]) ).
fof(f456,plain,
vangle(vd1361,vd1363,vd1362) = vangle(vd1361,vd1362,vd1363),
inference(cnf_transformation,[],[f15]) ).
fof(f457,plain,
vd1363 != vd1362,
inference(cnf_transformation,[],[f16]) ).
fof(f458,plain,
vd1363 != vd1361,
inference(cnf_transformation,[],[f17]) ).
fof(f459,plain,
vd1361 != vd1362,
inference(cnf_transformation,[],[f18]) ).
fof(f460,plain,
rpoint(sK5),
inference(cnf_transformation,[],[f357]) ).
fof(f461,plain,
vd1363 = sK5,
inference(cnf_transformation,[],[f357]) ).
fof(f462,plain,
rpoint(sK6),
inference(cnf_transformation,[],[f358]) ).
fof(f463,plain,
vd1361 = sK6,
inference(cnf_transformation,[],[f358]) ).
fof(f474,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,[],[f366]) ).
fof(f475,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,[],[f366]) ).
fof(f476,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,[],[f366]) ).
fof(f484,plain,
! [X3,X0,X1,X4] :
( vf(X0,X1) = sK7(X0,X1)
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f371]) ).
fof(f488,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f178]) ).
fof(f491,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,[],[f184]) ).
fof(f493,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,[],[f184]) ).
fof(f494,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,[],[f184]) ).
fof(f499,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,[],[f194]) ).
fof(f503,plain,
v0 = vd684,
inference(cnf_transformation,[],[f50]) ).
fof(f506,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X2,X3)
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f204]) ).
fof(f511,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,[],[f208]) ).
fof(f512,plain,
! [X2,X3,X0,X1,X4,X5] :
( vf(X0,X2) = vplus(vf(X0,X1),vf(X1,X2))
| ~ rR(X1,X0,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(cnf_transformation,[],[f210]) ).
fof(f516,plain,
! [X3,X0,X1,X4] :
( rline(sK10(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f376]) ).
fof(f517,plain,
! [X3,X0,X1,X4] :
( ron(X0,sK10(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f376]) ).
fof(f518,plain,
! [X3,X0,X1,X4] :
( ron(X1,sK10(X0,X1))
| X0 = X1
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f376]) ).
fof(f573,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rR(X1,X2,X3)
| ~ rR(X1,X0,X3)
| ~ rR(X1,X0,X2)
| X3 != X4
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f265]) ).
fof(f574,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,[],[f267]) ).
fof(f698,plain,
vf(vd1371,sK5) != vf(sK6,sK1),
inference(definition_unfolding,[],[f433,f461,f463,f440]) ).
fof(f699,plain,
vangle(vd1371,sK1,sK5) = vangle(sK6,sK5,sK1),
inference(definition_unfolding,[],[f434,f440,f461,f463,f461,f440]) ).
fof(f701,plain,
vf(sK6,sK5) = vf(sK1,vd1371),
inference(definition_unfolding,[],[f436,f463,f461,f440]) ).
fof(f702,plain,
rR(vd1371,sK1,sK6),
inference(definition_unfolding,[],[f437,f440,f463]) ).
fof(f705,plain,
vangle(sK6,sK5,sK1) = vangle(sK6,sK1,sK5),
inference(definition_unfolding,[],[f456,f463,f461,f440,f463,f440,f461]) ).
fof(f706,plain,
sK1 != sK5,
inference(definition_unfolding,[],[f457,f461,f440]) ).
fof(f707,plain,
sK5 != sK6,
inference(definition_unfolding,[],[f458,f461,f463]) ).
fof(f708,plain,
sK1 != sK6,
inference(definition_unfolding,[],[f459,f463,f440]) ).
fof(f709,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,[],[f476,f503]) ).
fof(f710,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,[],[f475,f503]) ).
fof(f711,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,[],[f474,f503]) ).
fof(f718,plain,
! [X2,X3,X0] :
( vf(X0,X2) = vf(X2,X0)
| ~ rpoint(X2)
| X0 != X3
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f441]) ).
fof(f719,plain,
! [X2,X3] :
( ~ rpoint(X3)
| ~ rpoint(X2)
| vf(X3,X2) = vf(X2,X3) ),
inference(equality_resolution,[],[f718]) ).
fof(f768,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X12] :
( vf(X1,X2) = vf(X4,X7)
| ron(X7,sK4(X3,X4,X7))
| vangle(X1,X0,X2) != vangle(X4,X3,X7)
| vf(X0,X2) != vf(X3,X7)
| vf(X0,X1) != vf(X3,X4)
| ~ rpoint(X7)
| X4 != X8
| ~ rpoint(X8)
| X3 != X9
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f453]) ).
fof(f769,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X12] :
( vf(X1,X2) = vf(X8,X7)
| ron(X7,sK4(X3,X8,X7))
| vangle(X1,X0,X2) != vangle(X8,X3,X7)
| vf(X0,X2) != vf(X3,X7)
| vf(X0,X1) != vf(X3,X8)
| ~ rpoint(X7)
| ~ rpoint(X8)
| X3 != X9
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f768]) ).
fof(f770,plain,
! [X2,X10,X0,X11,X1,X8,X9,X7,X12] :
( vf(X1,X2) = vf(X8,X7)
| ron(X7,sK4(X9,X8,X7))
| vangle(X1,X0,X2) != vangle(X8,X9,X7)
| vf(X0,X2) != vf(X9,X7)
| vf(X0,X1) != vf(X9,X8)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f769]) ).
fof(f771,plain,
! [X10,X0,X11,X1,X8,X9,X7,X12] :
( vf(X8,X7) = vf(X1,X10)
| ron(X7,sK4(X9,X8,X7))
| vangle(X8,X9,X7) != vangle(X1,X0,X10)
| vf(X9,X7) != vf(X0,X10)
| vf(X0,X1) != vf(X9,X8)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X1 = X10
| X0 = X10
| X0 = X1
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f770]) ).
fof(f772,plain,
! [X10,X0,X11,X8,X9,X7,X12] :
( vf(X8,X7) = vf(X11,X10)
| ron(X7,sK4(X9,X8,X7))
| vangle(X8,X9,X7) != vangle(X11,X0,X10)
| vf(X9,X7) != vf(X0,X10)
| vf(X9,X8) != vf(X0,X11)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X10 = X11
| X0 = X10
| X0 = X11
| ~ rpoint(X10)
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f771]) ).
fof(f773,plain,
! [X10,X11,X8,X9,X7,X12] :
( vangle(X8,X9,X7) != vangle(X11,X12,X10)
| ron(X7,sK4(X9,X8,X7))
| vf(X8,X7) = vf(X11,X10)
| vf(X9,X7) != vf(X12,X10)
| vf(X9,X8) != vf(X12,X11)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X10 = X11
| X10 = X12
| X11 = X12
| ~ rpoint(X10)
| ~ rpoint(X11)
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f772]) ).
fof(f774,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X12] :
( vf(X1,X2) = vf(X4,X7)
| ron(X4,sK4(X3,X4,X7))
| vangle(X1,X0,X2) != vangle(X4,X3,X7)
| vf(X0,X2) != vf(X3,X7)
| vf(X0,X1) != vf(X3,X4)
| ~ rpoint(X7)
| X4 != X8
| ~ rpoint(X8)
| X3 != X9
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f452]) ).
fof(f775,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X12] :
( vf(X1,X2) = vf(X8,X7)
| ron(X8,sK4(X3,X8,X7))
| vangle(X1,X0,X2) != vangle(X8,X3,X7)
| vf(X0,X2) != vf(X3,X7)
| vf(X0,X1) != vf(X3,X8)
| ~ rpoint(X7)
| ~ rpoint(X8)
| X3 != X9
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f774]) ).
fof(f776,plain,
! [X2,X10,X0,X11,X1,X8,X9,X7,X12] :
( vf(X1,X2) = vf(X8,X7)
| ron(X8,sK4(X9,X8,X7))
| vangle(X1,X0,X2) != vangle(X8,X9,X7)
| vf(X0,X2) != vf(X9,X7)
| vf(X0,X1) != vf(X9,X8)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f775]) ).
fof(f777,plain,
! [X10,X0,X11,X1,X8,X9,X7,X12] :
( vf(X8,X7) = vf(X1,X10)
| ron(X8,sK4(X9,X8,X7))
| vangle(X8,X9,X7) != vangle(X1,X0,X10)
| vf(X9,X7) != vf(X0,X10)
| vf(X0,X1) != vf(X9,X8)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X1 = X10
| X0 = X10
| X0 = X1
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f776]) ).
fof(f778,plain,
! [X10,X0,X11,X8,X9,X7,X12] :
( vf(X8,X7) = vf(X11,X10)
| ron(X8,sK4(X9,X8,X7))
| vangle(X8,X9,X7) != vangle(X11,X0,X10)
| vf(X9,X7) != vf(X0,X10)
| vf(X9,X8) != vf(X0,X11)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X10 = X11
| X0 = X10
| X0 = X11
| ~ rpoint(X10)
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f777]) ).
fof(f779,plain,
! [X10,X11,X8,X9,X7,X12] :
( vangle(X8,X9,X7) != vangle(X11,X12,X10)
| ron(X8,sK4(X9,X8,X7))
| vf(X8,X7) = vf(X11,X10)
| vf(X9,X7) != vf(X12,X10)
| vf(X9,X8) != vf(X12,X11)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X10 = X11
| X10 = X12
| X11 = X12
| ~ rpoint(X10)
| ~ rpoint(X11)
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f778]) ).
fof(f780,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X12] :
( vf(X1,X2) = vf(X4,X7)
| ron(X3,sK4(X3,X4,X7))
| vangle(X1,X0,X2) != vangle(X4,X3,X7)
| vf(X0,X2) != vf(X3,X7)
| vf(X0,X1) != vf(X3,X4)
| ~ rpoint(X7)
| X4 != X8
| ~ rpoint(X8)
| X3 != X9
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f451]) ).
fof(f781,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X12] :
( vf(X1,X2) = vf(X8,X7)
| ron(X3,sK4(X3,X8,X7))
| vangle(X1,X0,X2) != vangle(X8,X3,X7)
| vf(X0,X2) != vf(X3,X7)
| vf(X0,X1) != vf(X3,X8)
| ~ rpoint(X7)
| ~ rpoint(X8)
| X3 != X9
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f780]) ).
fof(f782,plain,
! [X2,X10,X0,X11,X1,X8,X9,X7,X12] :
( vf(X1,X2) = vf(X8,X7)
| ron(X9,sK4(X9,X8,X7))
| vangle(X1,X0,X2) != vangle(X8,X9,X7)
| vf(X0,X2) != vf(X9,X7)
| vf(X0,X1) != vf(X9,X8)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f781]) ).
fof(f783,plain,
! [X10,X0,X11,X1,X8,X9,X7,X12] :
( vf(X8,X7) = vf(X1,X10)
| ron(X9,sK4(X9,X8,X7))
| vangle(X8,X9,X7) != vangle(X1,X0,X10)
| vf(X9,X7) != vf(X0,X10)
| vf(X0,X1) != vf(X9,X8)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X1 = X10
| X0 = X10
| X0 = X1
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f782]) ).
fof(f784,plain,
! [X10,X0,X11,X8,X9,X7,X12] :
( vf(X8,X7) = vf(X11,X10)
| ron(X9,sK4(X9,X8,X7))
| vangle(X8,X9,X7) != vangle(X11,X0,X10)
| vf(X9,X7) != vf(X0,X10)
| vf(X9,X8) != vf(X0,X11)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X10 = X11
| X0 = X10
| X0 = X11
| ~ rpoint(X10)
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f783]) ).
fof(f785,plain,
! [X10,X11,X8,X9,X7,X12] :
( vangle(X8,X9,X7) != vangle(X11,X12,X10)
| ron(X9,sK4(X9,X8,X7))
| vf(X8,X7) = vf(X11,X10)
| vf(X9,X7) != vf(X12,X10)
| vf(X9,X8) != vf(X12,X11)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X10 = X11
| X10 = X12
| X11 = X12
| ~ rpoint(X10)
| ~ rpoint(X11)
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f784]) ).
fof(f786,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4,X12] :
( vf(X1,X2) = vf(X4,X7)
| rline(sK4(X3,X4,X7))
| vangle(X1,X0,X2) != vangle(X4,X3,X7)
| vf(X0,X2) != vf(X3,X7)
| vf(X0,X1) != vf(X3,X4)
| ~ rpoint(X7)
| X4 != X8
| ~ rpoint(X8)
| X3 != X9
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f450]) ).
fof(f787,plain,
! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X12] :
( vf(X1,X2) = vf(X8,X7)
| rline(sK4(X3,X8,X7))
| vangle(X1,X0,X2) != vangle(X8,X3,X7)
| vf(X0,X2) != vf(X3,X7)
| vf(X0,X1) != vf(X3,X8)
| ~ rpoint(X7)
| ~ rpoint(X8)
| X3 != X9
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f786]) ).
fof(f788,plain,
! [X2,X10,X0,X11,X1,X8,X9,X7,X12] :
( vf(X1,X2) = vf(X8,X7)
| rline(sK4(X9,X8,X7))
| vangle(X1,X0,X2) != vangle(X8,X9,X7)
| vf(X0,X2) != vf(X9,X7)
| vf(X0,X1) != vf(X9,X8)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X10
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f787]) ).
fof(f789,plain,
! [X10,X0,X11,X1,X8,X9,X7,X12] :
( vf(X8,X7) = vf(X1,X10)
| rline(sK4(X9,X8,X7))
| vangle(X8,X9,X7) != vangle(X1,X0,X10)
| vf(X9,X7) != vf(X0,X10)
| vf(X0,X1) != vf(X9,X8)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X1 = X10
| X0 = X10
| X0 = X1
| ~ rpoint(X10)
| X1 != X11
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f788]) ).
fof(f790,plain,
! [X10,X0,X11,X8,X9,X7,X12] :
( vf(X8,X7) = vf(X11,X10)
| rline(sK4(X9,X8,X7))
| vangle(X8,X9,X7) != vangle(X11,X0,X10)
| vf(X9,X7) != vf(X0,X10)
| vf(X9,X8) != vf(X0,X11)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X10 = X11
| X0 = X10
| X0 = X11
| ~ rpoint(X10)
| ~ rpoint(X11)
| X0 != X12
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f789]) ).
fof(f791,plain,
! [X10,X11,X8,X9,X7,X12] :
( vangle(X8,X9,X7) != vangle(X11,X12,X10)
| rline(sK4(X9,X8,X7))
| vf(X8,X7) = vf(X11,X10)
| vf(X9,X7) != vf(X12,X10)
| vf(X9,X8) != vf(X12,X11)
| ~ rpoint(X7)
| ~ rpoint(X8)
| ~ rpoint(X9)
| X10 = X11
| X10 = X12
| X11 = X12
| ~ rpoint(X10)
| ~ rpoint(X11)
| ~ rpoint(X12) ),
inference(equality_resolution,[],[f790]) ).
fof(f838,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,[],[f709]) ).
fof(f839,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,[],[f838]) ).
fof(f840,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,[],[f839]) ).
fof(f841,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,[],[f840]) ).
fof(f842,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,[],[f710]) ).
fof(f843,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,[],[f842]) ).
fof(f844,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,[],[f843]) ).
fof(f845,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,[],[f844]) ).
fof(f846,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,[],[f711]) ).
fof(f847,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,[],[f846]) ).
fof(f848,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,[],[f847]) ).
fof(f849,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,[],[f848]) ).
fof(f863,plain,
! [X3,X0,X4] :
( vf(X0,X3) = sK7(X0,X3)
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f484]) ).
fof(f864,plain,
! [X3,X4] :
( ~ rpoint(X4)
| ~ rpoint(X3)
| vf(X4,X3) = sK7(X4,X3) ),
inference(equality_resolution,[],[f863]) ).
fof(f873,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1)
| ~ ron(X2,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f488]) ).
fof(f874,plain,
! [X0,X1,X6,X7,X4,X5] :
( rR(X1,X0,X5)
| rR(X0,X1,X5)
| rR(X5,X0,X1)
| ~ ron(X5,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rline(X4)
| X1 = X5
| X0 = X5
| X0 = X1
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f873]) ).
fof(f875,plain,
! [X0,X6,X7,X4,X5] :
( rR(X6,X0,X5)
| rR(X0,X6,X5)
| rR(X5,X0,X6)
| ~ ron(X5,X4)
| ~ ron(X6,X4)
| ~ ron(X0,X4)
| ~ rline(X4)
| X5 = X6
| X0 = X5
| X0 = X6
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f874]) ).
fof(f876,plain,
! [X6,X7,X4,X5] :
( ~ ron(X7,X4)
| rR(X7,X6,X5)
| rR(X5,X7,X6)
| ~ ron(X5,X4)
| ~ ron(X6,X4)
| rR(X6,X7,X5)
| ~ rline(X4)
| X5 = X6
| X5 = X7
| X6 = X7
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f875]) ).
fof(f885,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,[],[f494]) ).
fof(f886,plain,
! [X3,X0,X4,X5] :
( ~ rR(X0,X4,X3)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f885]) ).
fof(f887,plain,
! [X3,X4,X5] :
( ~ rR(X5,X4,X3)
| ~ rR(X4,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f886]) ).
fof(f888,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,[],[f493]) ).
fof(f889,plain,
! [X3,X1,X4,X5] :
( ~ rR(X1,X3,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f888]) ).
fof(f890,plain,
! [X3,X4,X5] :
( ~ rR(X4,X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X3 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f889]) ).
fof(f891,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f890]) ).
fof(f896,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,[],[f491]) ).
fof(f897,plain,
! [X3,X0,X4,X5] :
( rR(X4,X3,X0)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f896]) ).
fof(f898,plain,
! [X3,X4,X5] :
( ~ rR(X4,X5,X3)
| rR(X4,X3,X5)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f897]) ).
fof(f909,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,[],[f499]) ).
fof(f910,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,[],[f909]) ).
fof(f911,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,[],[f910]) ).
fof(f921,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ron(X2,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f506]) ).
fof(f922,plain,
! [X0,X1,X6,X7,X4,X5] :
( ron(X5,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rR(X1,X0,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f921]) ).
fof(f923,plain,
! [X0,X6,X7,X4,X5] :
( ron(X5,X4)
| ~ ron(X6,X4)
| ~ ron(X0,X4)
| ~ rR(X6,X0,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f922]) ).
fof(f924,plain,
! [X6,X7,X4,X5] :
( ~ rR(X6,X7,X5)
| ~ ron(X6,X4)
| ~ ron(X7,X4)
| ron(X5,X4)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f923]) ).
fof(f941,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,[],[f511]) ).
fof(f942,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,[],[f941]) ).
fof(f943,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,[],[f942]) ).
fof(f944,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,[],[f943]) ).
fof(f945,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,[],[f944]) ).
fof(f946,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,[],[f945]) ).
fof(f947,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,[],[f946]) ).
fof(f948,plain,
! [X3,X0,X1,X4,X5] :
( vf(X0,X3) = vplus(vf(X0,X1),vf(X1,X3))
| ~ rR(X1,X0,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f512]) ).
fof(f949,plain,
! [X3,X0,X4,X5] :
( vf(X0,X3) = vplus(vf(X0,X4),vf(X4,X3))
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f948]) ).
fof(f950,plain,
! [X3,X4,X5] :
( ~ rR(X4,X5,X3)
| vf(X5,X3) = vplus(vf(X5,X4),vf(X4,X3))
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f949]) ).
fof(f957,plain,
! [X3,X0,X4] :
( ron(X3,sK10(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f518]) ).
fof(f958,plain,
! [X3,X4] :
( ron(X3,sK10(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f957]) ).
fof(f959,plain,
! [X3,X0,X4] :
( ron(X0,sK10(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f517]) ).
fof(f960,plain,
! [X3,X4] :
( ron(X4,sK10(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f959]) ).
fof(f961,plain,
! [X3,X0,X4] :
( rline(sK10(X0,X3))
| X0 = X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f516]) ).
fof(f962,plain,
! [X3,X4] :
( rline(sK10(X4,X3))
| X3 = X4
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f961]) ).
fof(f1136,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ~ rR(X1,X2,X4)
| ~ rR(X1,X0,X4)
| ~ rR(X1,X0,X2)
| ~ rpoint(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f573]) ).
fof(f1137,plain,
! [X0,X1,X6,X7,X4,X5] :
( ~ rR(X1,X5,X4)
| ~ rR(X1,X0,X4)
| ~ rR(X1,X0,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1136]) ).
fof(f1138,plain,
! [X0,X6,X7,X4,X5] :
( ~ rR(X6,X5,X4)
| ~ rR(X6,X0,X4)
| ~ rR(X6,X0,X5)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1137]) ).
fof(f1139,plain,
! [X6,X7,X4,X5] :
( ~ rR(X6,X7,X5)
| ~ rR(X6,X7,X4)
| ~ rR(X6,X5,X4)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1138]) ).
fof(f1140,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,[],[f574]) ).
fof(f1141,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,[],[f1140]) ).
fof(f1142,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,[],[f1141]) ).
fof(f1143,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,[],[f1142]) ).
fof(f1498,definition,
sF52 = vf(vd1371,sK5),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f1499,plain,
vf(vd1371,sK5) = sF52,
inference(reorient_equations,[],[f1498]) ).
fof(f1500,definition,
sF53 = vf(sK6,sK1),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f1501,plain,
vf(sK6,sK1) = sF53,
inference(reorient_equations,[],[f1500]) ).
fof(f1502,plain,
sF52 != sF53,
inference(definition_folding,[],[f698,f1501,f1499]) ).
fof(f1504,plain,
! [X4,X5] :
( ~ rR(X4,X5,X5)
| ~ rpoint(X5)
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f891]) ).
fof(f1553,plain,
vangle(vd1371,sK1,sK5) = vangle(sK6,sK1,sK5),
inference(forward_demodulation,[],[f699,f705]) ).
fof(f1555,plain,
( rR(vd1371,sK6,sK1)
| ~ rpoint(sK6)
| ~ rpoint(vd1371)
| ~ rpoint(sK1) ),
inference(resolution,[],[f898,f702]) ).
fof(f1556,plain,
( rR(vd1371,sK6,sK1)
| ~ rpoint(vd1371)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f1555,f462]) ).
fof(f1557,plain,
( rR(vd1371,sK6,sK1)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f1556,f438]) ).
fof(f1558,plain,
rR(vd1371,sK6,sK1),
inference(forward_subsumption_resolution,[],[f1557,f439]) ).
fof(f1560,plain,
! [X0] :
( ~ rpoint(X0)
| vf(vd1371,X0) = vf(X0,vd1371) ),
inference(resolution,[],[f719,f438]) ).
fof(f1562,plain,
! [X0] :
( ~ rpoint(X0)
| vf(sK5,X0) = vf(X0,sK5) ),
inference(resolution,[],[f719,f460]) ).
fof(f1563,plain,
! [X0] :
( ~ rpoint(X0)
| vf(sK6,X0) = vf(X0,sK6) ),
inference(resolution,[],[f719,f462]) ).
fof(f1577,definition,
( spl54_13
<=> vd1371 = sK1 ),
introduced(definition,[new_symbols(definition,[spl54_13])],[avatar_definition]) ).
fof(f1578,plain,
( vd1371 != sK1
| spl54_13 ),
inference(avatar_component_clause,[],[f1577]) ).
fof(f1579,plain,
( vd1371 = sK1
| ~ spl54_13 ),
inference(avatar_component_clause,[],[f1577]) ).
fof(f1587,definition,
( spl54_15
<=> vd1371 = sK5 ),
introduced(definition,[new_symbols(definition,[spl54_15])],[avatar_definition]) ).
fof(f1588,plain,
( vd1371 != sK5
| spl54_15 ),
inference(avatar_component_clause,[],[f1587]) ).
fof(f1589,plain,
( vd1371 = sK5
| ~ spl54_15 ),
inference(avatar_component_clause,[],[f1587]) ).
fof(f1746,plain,
vf(vd1371,sK5) = vf(sK5,vd1371),
inference(resolution,[],[f1560,f460]) ).
fof(f1747,plain,
vf(vd1371,sK6) = vf(sK6,vd1371),
inference(resolution,[],[f1560,f462]) ).
fof(f1833,plain,
sF52 = vf(sK5,vd1371),
inference(forward_demodulation,[],[f1746,f1499]) ).
fof(f1940,plain,
vf(sK6,sK1) = vf(sK1,sK6),
inference(resolution,[],[f1563,f439]) ).
fof(f1941,plain,
vf(sK6,sK5) = vf(sK5,sK6),
inference(resolution,[],[f1563,f460]) ).
fof(f1943,plain,
sF53 = vf(sK1,sK6),
inference(forward_demodulation,[],[f1940,f1501]) ).
fof(f1975,plain,
vf(sK5,sK1) = vf(sK1,sK5),
inference(resolution,[],[f1562,f439]) ).
fof(f2011,plain,
! [X0,X1] :
( ~ rpoint(X1)
| sK5 = X1
| ~ rpoint(X0)
| sK5 = X0
| vangle(X0,X1,sK5) = vangle(sK5,X1,X0) ),
inference(resolution,[],[f911,f460]) ).
fof(f2122,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,[],[f849,f958]) ).
fof(f2125,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,[],[f2122]) ).
fof(f2127,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,[],[f2125,f962]) ).
fof(f2128,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,[],[f2127,f958]) ).
fof(f2131,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,[],[f2128]) ).
fof(f2132,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,[],[f2131,f1504]) ).
fof(f2138,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,[],[f2132,f960]) ).
fof(f2139,plain,
! [X0,X1] :
( ~ rpoint(X1)
| X0 = X1
| ~ rpoint(X0)
| vd684 = vangle(X0,X1,X0) ),
inference(duplicate_literal_removal,[],[f2138]) ).
fof(f2143,plain,
! [X0] :
( ~ rpoint(X0)
| sK1 = X0
| vd684 = vangle(X0,sK1,X0) ),
inference(resolution,[],[f2139,f439]) ).
fof(f2144,plain,
! [X0] :
( ~ rpoint(X0)
| sK5 = X0
| vd684 = vangle(X0,sK5,X0) ),
inference(resolution,[],[f2139,f460]) ).
fof(f2150,plain,
( sK1 = sK6
| vd684 = vangle(sK6,sK1,sK6) ),
inference(resolution,[],[f2143,f462]) ).
fof(f2151,plain,
vd684 = vangle(sK6,sK1,sK6),
inference(forward_subsumption_resolution,[],[f2150,f708]) ).
fof(f2158,plain,
( sK5 = sK6
| vd684 = vangle(sK6,sK5,sK6) ),
inference(resolution,[],[f2144,f462]) ).
fof(f2159,plain,
vd684 = vangle(sK6,sK5,sK6),
inference(forward_subsumption_resolution,[],[f2158,f707]) ).
fof(f2174,definition,
( spl54_73
<=> vd1371 = sK6 ),
introduced(definition,[new_symbols(definition,[spl54_73])],[avatar_definition]) ).
fof(f2175,plain,
( vd1371 != sK6
| spl54_73 ),
inference(avatar_component_clause,[],[f2174]) ).
fof(f2176,plain,
( vd1371 = sK6
| ~ spl54_73 ),
inference(avatar_component_clause,[],[f2174]) ).
fof(f2186,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( rR(X0,X1,X2)
| rR(X0,X3,X4)
| X0 = X2
| X0 = X4
| X0 = X1
| X0 = X3
| ~ ron(X2,X5)
| ~ ron(X1,X5)
| ~ ron(X4,sK10(X6,X0))
| ~ ron(X3,sK10(X6,X0))
| vangle(X4,X0,X2) = vangle(X3,X0,X1)
| ~ rline(X5)
| ~ rline(sK10(X6,X0))
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| X0 = X6
| ~ rpoint(X0)
| ~ rpoint(X6) ),
inference(resolution,[],[f947,f958]) ).
fof(f2189,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( rR(X0,X1,X2)
| rR(X0,X3,X4)
| X0 = X2
| X0 = X4
| X0 = X1
| X0 = X3
| ~ ron(X2,X5)
| ~ ron(X1,X5)
| ~ ron(X4,sK10(X6,X0))
| ~ ron(X3,sK10(X6,X0))
| vangle(X4,X0,X2) = vangle(X3,X0,X1)
| ~ rline(X5)
| ~ rline(sK10(X6,X0))
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| X0 = X6
| ~ rpoint(X6) ),
inference(duplicate_literal_removal,[],[f2186]) ).
fof(f2191,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ ron(X4,sK10(X6,X0))
| rR(X0,X3,X4)
| X0 = X2
| X0 = X4
| X0 = X1
| X0 = X3
| ~ ron(X2,X5)
| ~ ron(X1,X5)
| rR(X0,X1,X2)
| ~ ron(X3,sK10(X6,X0))
| vangle(X4,X0,X2) = vangle(X3,X0,X1)
| ~ rline(X5)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X0)
| X0 = X6
| ~ rpoint(X6) ),
inference(forward_subsumption_resolution,[],[f2189,f962]) ).
fof(f2371,plain,
! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ~ rR(sK5,sK6,sK1)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| sK1 = sK5
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ rpoint(sK5) ),
inference(superposition,[],[f841,f705]) ).
fof(f2386,plain,
! [X0] :
( ~ rR(X0,sK1,vd1371)
| rR(X0,sK1,sK6)
| ~ rpoint(X0)
| ~ rpoint(sK6)
| ~ rpoint(vd1371)
| ~ rpoint(sK1) ),
inference(resolution,[],[f1143,f702]) ).
fof(f2387,plain,
! [X0] :
( ~ rR(X0,sK6,vd1371)
| rR(X0,sK6,sK1)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ rpoint(sK6) ),
inference(resolution,[],[f1143,f1558]) ).
fof(f2391,plain,
! [X0] :
( ~ rR(X0,sK6,vd1371)
| rR(X0,sK6,sK1)
| ~ rpoint(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f2387,f439]) ).
fof(f2392,plain,
! [X0] :
( ~ rR(X0,sK1,vd1371)
| rR(X0,sK1,sK6)
| ~ rpoint(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f2386,f462]) ).
fof(f2393,plain,
! [X0] :
( ~ rR(X0,sK6,vd1371)
| rR(X0,sK6,sK1)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f2391,f438]) ).
fof(f2394,plain,
! [X0] :
( ~ rR(X0,sK1,vd1371)
| rR(X0,sK1,sK6)
| ~ rpoint(X0)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f2392,f438]) ).
fof(f2395,plain,
! [X0] :
( ~ rR(X0,sK6,vd1371)
| rR(X0,sK6,sK1)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2393,f462]) ).
fof(f2396,plain,
! [X0] :
( ~ rR(X0,sK1,vd1371)
| rR(X0,sK1,sK6)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f2394,f439]) ).
fof(f2419,plain,
( ~ rR(sK1,vd1371,sK6)
| ~ rpoint(sK6)
| ~ rpoint(sK1)
| ~ rpoint(vd1371) ),
inference(resolution,[],[f887,f702]) ).
fof(f2437,plain,
! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ron(sK1,X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| sK1 = sK5
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ rpoint(sK5) ),
inference(superposition,[],[f845,f705]) ).
fof(f2515,plain,
! [X0] :
( sK1 = sK5
| ~ rpoint(X0)
| sK5 = X0
| vangle(sK5,sK1,X0) = vangle(X0,sK1,sK5) ),
inference(resolution,[],[f2011,f439]) ).
fof(f2519,plain,
! [X0] :
( ~ rpoint(X0)
| sK5 = X0
| vangle(sK5,sK1,X0) = vangle(X0,sK1,sK5) ),
inference(forward_subsumption_resolution,[],[f2515,f706]) ).
fof(f2528,plain,
( vd1371 = sK5
| vangle(vd1371,sK1,sK5) = vangle(sK5,sK1,vd1371) ),
inference(resolution,[],[f2519,f438]) ).
fof(f2534,plain,
( vangle(vd1371,sK1,sK5) = vangle(sK5,sK1,vd1371)
| spl54_15 ),
inference(forward_subsumption_resolution,[],[f2528,f1588]) ).
fof(f2535,plain,
( vangle(sK6,sK1,sK5) = vangle(sK5,sK1,vd1371)
| spl54_15 ),
inference(forward_demodulation,[],[f2534,f1553]) ).
fof(f2536,plain,
( ! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ron(vd1371,X0)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| vd1371 = sK1
| sK1 = sK5
| ~ rline(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK1) )
| spl54_15 ),
inference(superposition,[],[f845,f2535]) ).
fof(f2844,plain,
! [X0] :
( ~ rpoint(X0)
| vf(sK1,X0) = sK7(sK1,X0) ),
inference(resolution,[],[f864,f439]) ).
fof(f2845,plain,
! [X0] :
( ~ rpoint(X0)
| vf(sK5,X0) = sK7(sK5,X0) ),
inference(resolution,[],[f864,f460]) ).
fof(f2846,plain,
! [X0] :
( ~ rpoint(X0)
| vf(sK6,X0) = sK7(sK6,X0) ),
inference(resolution,[],[f864,f462]) ).
fof(f2847,plain,
vf(sK6,vd1371) = sK7(sK6,vd1371),
inference(resolution,[],[f2846,f438]) ).
fof(f2850,plain,
vf(sK6,sK5) = sK7(sK6,sK5),
inference(resolution,[],[f2846,f460]) ).
fof(f2857,plain,
vf(sK1,sK5) = sK7(sK1,sK5),
inference(resolution,[],[f2844,f460]) ).
fof(f2863,plain,
vf(sK5,vd1371) = sK7(sK5,vd1371),
inference(resolution,[],[f2845,f438]) ).
fof(f2867,plain,
vf(sK5,sK6) = sK7(sK5,sK6),
inference(resolution,[],[f2845,f462]) ).
fof(f2868,plain,
vf(sK6,sK5) = sK7(sK5,sK6),
inference(forward_demodulation,[],[f2867,f1941]) ).
fof(f2871,plain,
sF52 = sK7(sK5,vd1371),
inference(forward_demodulation,[],[f2863,f1833]) ).
fof(f2872,plain,
sK7(sK6,sK5) = sK7(sK5,sK6),
inference(forward_demodulation,[],[f2868,f2850]) ).
fof(f2874,plain,
( vf(sK1,sK6) = vplus(vf(sK1,vd1371),vf(vd1371,sK6))
| ~ rpoint(sK6)
| ~ rpoint(vd1371)
| ~ rpoint(sK1) ),
inference(resolution,[],[f950,f702]) ).
fof(f2880,plain,
( vf(sK1,sK6) = vplus(vf(sK1,vd1371),vf(vd1371,sK6))
| ~ rpoint(vd1371)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f2874,f462]) ).
fof(f2882,plain,
( vf(sK1,sK6) = vplus(vf(sK1,vd1371),vf(vd1371,sK6))
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f2880,f438]) ).
fof(f2884,plain,
vf(sK1,sK6) = vplus(vf(sK1,vd1371),vf(vd1371,sK6)),
inference(forward_subsumption_resolution,[],[f2882,f439]) ).
fof(f2886,plain,
vf(sK1,sK6) = vplus(vf(sK1,vd1371),vf(sK6,vd1371)),
inference(forward_demodulation,[],[f2884,f1747]) ).
fof(f2888,plain,
vf(sK1,sK6) = vplus(vf(sK1,vd1371),sK7(sK6,vd1371)),
inference(forward_demodulation,[],[f2886,f2847]) ).
fof(f2890,plain,
vf(sK1,sK6) = vplus(vf(sK6,sK5),sK7(sK6,vd1371)),
inference(forward_demodulation,[],[f2888,f701]) ).
fof(f2892,plain,
vf(sK1,sK6) = vplus(sK7(sK6,sK5),sK7(sK6,vd1371)),
inference(forward_demodulation,[],[f2890,f2850]) ).
fof(f2893,plain,
sF53 = vplus(sK7(sK6,sK5),sK7(sK6,vd1371)),
inference(forward_demodulation,[],[f2892,f1943]) ).
fof(f3107,plain,
( vf(sK6,sK5) = vf(sK1,sK6)
| ~ spl54_73 ),
inference(superposition,[],[f701,f2176]) ).
fof(f3125,plain,
( sF52 = sK7(sK5,sK6)
| ~ spl54_73 ),
inference(superposition,[],[f2871,f2176]) ).
fof(f3130,plain,
( sF52 = sK7(sK6,sK5)
| ~ spl54_73 ),
inference(forward_demodulation,[],[f3125,f2872]) ).
fof(f3139,plain,
( vf(sK6,sK5) = sF53
| ~ spl54_73 ),
inference(forward_demodulation,[],[f3107,f1943]) ).
fof(f3145,plain,
( sF53 = sK7(sK6,sK5)
| ~ spl54_73 ),
inference(forward_demodulation,[],[f3139,f2850]) ).
fof(f3146,plain,
( sF52 = sF53
| ~ spl54_73 ),
inference(forward_demodulation,[],[f3145,f3130]) ).
fof(f3147,plain,
( $false
| ~ spl54_73 ),
inference(forward_subsumption_resolution,[],[f3146,f1502]) ).
fof(f3148,plain,
~ spl54_73,
inference(avatar_contradiction_clause,[],[f3147]) ).
fof(f4002,plain,
! [X2,X3,X0,X1] :
( rR(X0,X1,X2)
| rR(X2,X0,X1)
| ~ ron(X2,sK10(X0,X3))
| ~ ron(X1,sK10(X0,X3))
| rR(X1,X0,X2)
| ~ rline(sK10(X0,X3))
| X1 = X2
| X0 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X3
| ~ rpoint(X3)
| ~ rpoint(X0) ),
inference(resolution,[],[f876,f960]) ).
fof(f4005,plain,
! [X2,X3,X0,X1] :
( rR(X0,X1,X2)
| rR(X2,X0,X1)
| ~ ron(X2,sK10(X0,X3))
| ~ ron(X1,sK10(X0,X3))
| rR(X1,X0,X2)
| ~ rline(sK10(X0,X3))
| X1 = X2
| X0 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X3
| ~ rpoint(X3) ),
inference(duplicate_literal_removal,[],[f4002]) ).
fof(f4802,plain,
! [X0] :
( ~ ron(vd1371,X0)
| ~ ron(sK1,X0)
| ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(vd1371)
| ~ rpoint(sK1) ),
inference(resolution,[],[f924,f702]) ).
fof(f4803,plain,
! [X0] :
( ~ ron(vd1371,X0)
| ~ ron(sK6,X0)
| ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ rpoint(sK6) ),
inference(resolution,[],[f924,f1558]) ).
fof(f6114,plain,
! [X0] :
( ~ rR(vd1371,sK6,X0)
| ~ rR(vd1371,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ rpoint(sK6) ),
inference(resolution,[],[f1139,f1558]) ).
fof(f6123,plain,
! [X0] :
( ~ rR(vd1371,sK6,X0)
| ~ rR(vd1371,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f6114,f439]) ).
fof(f6126,plain,
! [X0] :
( ~ rR(vd1371,sK6,X0)
| ~ rR(vd1371,sK1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f6123,f438]) ).
fof(f6129,plain,
! [X0] :
( ~ rR(vd1371,sK6,X0)
| ~ rR(vd1371,sK1,X0)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f6126,f462]) ).
fof(f9753,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK5,sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| ~ rpoint(sK5)
| ~ rpoint(vd1371)
| ~ rpoint(sK1)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(superposition,[],[f773,f1553]) ).
fof(f9781,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK5,sK6,sK1))
| vf(X0,X2) = vf(sK6,sK1)
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(superposition,[],[f773,f705]) ).
fof(f9836,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK5,sK6,sK1))
| vf(X0,X2) = vf(sK6,sK1)
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f9781,f439]) ).
fof(f9864,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK5,sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| ~ rpoint(vd1371)
| ~ rpoint(sK1)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f9753,f460]) ).
fof(f9882,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK5,sK6,sK1))
| vf(X0,X2) = vf(sK6,sK1)
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| ~ rpoint(sK5)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f9836,f462]) ).
fof(f9910,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK5,sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| ~ rpoint(sK1)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f9864,f438]) ).
fof(f9928,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK5,sK6,sK1))
| vf(X0,X2) = vf(sK6,sK1)
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f9882,f460]) ).
fof(f9956,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK5,sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f9910,f439]) ).
fof(f9974,plain,
! [X2,X0,X1] :
( vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK5,sK6,sK1))
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f9928,f1501]) ).
fof(f10002,plain,
! [X2,X0,X1] :
( vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK5,sK4(sK1,vd1371,sK5))
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f9956,f1499]) ).
fof(f10020,plain,
! [X2,X0,X1] :
( vf(X1,X2) != vf(sK1,sK5)
| vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK5,sK6,sK1))
| vf(X1,X0) != vf(sK5,sK6)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f9974,f1975]) ).
fof(f10047,plain,
! [X2,X0,X1] :
( vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK5,sK4(sK1,vd1371,sK5))
| vf(X1,X0) != vf(sK1,vd1371)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10002,f2857]) ).
fof(f10065,plain,
! [X2,X0,X1] :
( vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK5,sK6,sK1))
| vf(X1,X0) != vf(sK5,sK6)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10020,f2857]) ).
fof(f10089,plain,
! [X2,X0,X1] :
( vf(X1,X0) != vf(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK5,sK4(sK1,vd1371,sK5))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10047,f701]) ).
fof(f10114,plain,
! [X2,X0,X1] :
( vf(X1,X0) != vf(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK5,sK6,sK1))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10065,f1941]) ).
fof(f10167,plain,
! [X2,X0,X1] :
( vf(X1,X0) != sK7(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK5,sK4(sK1,vd1371,sK5))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10089,f2850]) ).
fof(f10184,plain,
! [X2,X0,X1] :
( vf(X1,X0) != sK7(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK5,sK6,sK1))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10114,f2850]) ).
fof(f10230,definition,
( spl54_587
<=> ron(sK5,sK4(sK1,vd1371,sK5)) ),
introduced(definition,[new_symbols(definition,[spl54_587])],[avatar_definition]) ).
fof(f10232,plain,
( ron(sK5,sK4(sK1,vd1371,sK5))
| ~ spl54_587 ),
inference(avatar_component_clause,[],[f10230]) ).
fof(f10234,definition,
( spl54_588
<=> ! [X2,X0,X1] :
( vf(X1,X0) != sK7(sK6,sK5)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X0 = X1
| X1 = X2
| X0 = X2
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| vf(X0,X2) = sF52
| vf(X1,X2) != sK7(sK1,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl54_588])],[avatar_definition]) ).
fof(f10235,plain,
( ! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X0 = X1
| X1 = X2
| X0 = X2
| vf(X1,X0) != sK7(sK6,sK5)
| vf(X0,X2) = sF52
| vf(X1,X2) != sK7(sK1,sK5) )
| ~ spl54_588 ),
inference(avatar_component_clause,[],[f10234]) ).
fof(f10236,plain,
( spl54_587
| spl54_588 ),
inference(avatar_split_clause,[],[f10167,f10234,f10230]) ).
fof(f10258,definition,
( spl54_590
<=> ron(sK1,sK4(sK5,sK6,sK1)) ),
introduced(definition,[new_symbols(definition,[spl54_590])],[avatar_definition]) ).
fof(f10260,plain,
( ron(sK1,sK4(sK5,sK6,sK1))
| ~ spl54_590 ),
inference(avatar_component_clause,[],[f10258]) ).
fof(f10262,definition,
( spl54_591
<=> ! [X2,X0,X1] :
( vf(X1,X0) != sK7(sK6,sK5)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X0 = X1
| X1 = X2
| X0 = X2
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| vf(X0,X2) = sF53
| vf(X1,X2) != sK7(sK1,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl54_591])],[avatar_definition]) ).
fof(f10263,plain,
( ! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X0 = X1
| X1 = X2
| X0 = X2
| vf(X1,X0) != sK7(sK6,sK5)
| vf(X0,X2) = sF53
| vf(X1,X2) != sK7(sK1,sK5) )
| ~ spl54_591 ),
inference(avatar_component_clause,[],[f10262]) ).
fof(f10264,plain,
( spl54_590
| spl54_591 ),
inference(avatar_split_clause,[],[f10184,f10262,f10258]) ).
fof(f10594,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(vd1371,sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| ~ rpoint(sK5)
| ~ rpoint(vd1371)
| ~ rpoint(sK1)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(superposition,[],[f779,f1553]) ).
fof(f10622,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK6,sK4(sK5,sK6,sK1))
| vf(X0,X2) = vf(sK6,sK1)
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(superposition,[],[f779,f705]) ).
fof(f10676,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK6,sK4(sK5,sK6,sK1))
| vf(X0,X2) = vf(sK6,sK1)
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f10622,f439]) ).
fof(f10703,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(vd1371,sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| ~ rpoint(vd1371)
| ~ rpoint(sK1)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f10594,f460]) ).
fof(f10720,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK6,sK4(sK5,sK6,sK1))
| vf(X0,X2) = vf(sK6,sK1)
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| ~ rpoint(sK5)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f10676,f462]) ).
fof(f10747,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(vd1371,sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| ~ rpoint(sK1)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f10703,f438]) ).
fof(f10764,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK6,sK4(sK5,sK6,sK1))
| vf(X0,X2) = vf(sK6,sK1)
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f10720,f460]) ).
fof(f10791,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(vd1371,sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f10747,f439]) ).
fof(f10808,plain,
! [X2,X0,X1] :
( vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK6,sK4(sK5,sK6,sK1))
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10764,f1501]) ).
fof(f10835,plain,
! [X2,X0,X1] :
( vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(vd1371,sK4(sK1,vd1371,sK5))
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10791,f1499]) ).
fof(f10852,plain,
! [X2,X0,X1] :
( vf(X1,X2) != vf(sK1,sK5)
| vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK6,sK4(sK5,sK6,sK1))
| vf(X1,X0) != vf(sK5,sK6)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10808,f1975]) ).
fof(f10878,plain,
! [X2,X0,X1] :
( vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(vd1371,sK4(sK1,vd1371,sK5))
| vf(X1,X0) != vf(sK1,vd1371)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10835,f2857]) ).
fof(f10895,plain,
! [X2,X0,X1] :
( vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK6,sK4(sK5,sK6,sK1))
| vf(X1,X0) != vf(sK5,sK6)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10852,f2857]) ).
fof(f10918,plain,
! [X2,X0,X1] :
( vf(X1,X0) != vf(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(vd1371,sK4(sK1,vd1371,sK5))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10878,f701]) ).
fof(f10934,plain,
! [X2,X0,X1] :
( vf(X1,X0) != vf(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK6,sK4(sK5,sK6,sK1))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10895,f1941]) ).
fof(f10956,plain,
! [X2,X0,X1] :
( vf(X1,X0) != sK7(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(vd1371,sK4(sK1,vd1371,sK5))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10918,f2850]) ).
fof(f10972,plain,
! [X2,X0,X1] :
( vf(X1,X0) != sK7(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK6,sK4(sK5,sK6,sK1))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f10934,f2850]) ).
fof(f11004,definition,
( spl54_656
<=> ron(vd1371,sK4(sK1,vd1371,sK5)) ),
introduced(definition,[new_symbols(definition,[spl54_656])],[avatar_definition]) ).
fof(f11006,plain,
( ron(vd1371,sK4(sK1,vd1371,sK5))
| ~ spl54_656 ),
inference(avatar_component_clause,[],[f11004]) ).
fof(f11007,plain,
( spl54_656
| spl54_588 ),
inference(avatar_split_clause,[],[f10956,f10234,f11004]) ).
fof(f11023,definition,
( spl54_657
<=> ron(sK6,sK4(sK5,sK6,sK1)) ),
introduced(definition,[new_symbols(definition,[spl54_657])],[avatar_definition]) ).
fof(f11025,plain,
( ron(sK6,sK4(sK5,sK6,sK1))
| ~ spl54_657 ),
inference(avatar_component_clause,[],[f11023]) ).
fof(f11026,plain,
( spl54_657
| spl54_591 ),
inference(avatar_split_clause,[],[f10972,f10262,f11023]) ).
fof(f11081,plain,
( vangle(sK6,sK1,sK5) != vangle(sK6,sK1,sK5)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK1)
| sK5 = sK6
| sK1 = sK5
| sK1 = sK6
| vf(sK5,sK6) != sK7(sK6,sK5)
| vf(sK6,sK1) = sF52
| vf(sK5,sK1) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(superposition,[],[f10235,f705]) ).
fof(f11083,plain,
( ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK1)
| sK5 = sK6
| sK1 = sK5
| sK1 = sK6
| vf(sK5,sK6) != sK7(sK6,sK5)
| vf(sK6,sK1) = sF52
| vf(sK5,sK1) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(trivial_inequality_removal,[],[f11081]) ).
fof(f11089,plain,
( ~ rpoint(sK6)
| ~ rpoint(sK1)
| sK5 = sK6
| sK1 = sK5
| sK1 = sK6
| vf(sK5,sK6) != sK7(sK6,sK5)
| vf(sK6,sK1) = sF52
| vf(sK5,sK1) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(forward_subsumption_resolution,[],[f11083,f460]) ).
fof(f11101,plain,
( ~ rpoint(sK1)
| sK5 = sK6
| sK1 = sK5
| sK1 = sK6
| vf(sK5,sK6) != sK7(sK6,sK5)
| vf(sK6,sK1) = sF52
| vf(sK5,sK1) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(forward_subsumption_resolution,[],[f11089,f462]) ).
fof(f11113,plain,
( sK5 = sK6
| sK1 = sK5
| sK1 = sK6
| vf(sK5,sK6) != sK7(sK6,sK5)
| vf(sK6,sK1) = sF52
| vf(sK5,sK1) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(forward_subsumption_resolution,[],[f11101,f439]) ).
fof(f11125,plain,
( sK1 = sK5
| sK1 = sK6
| vf(sK5,sK6) != sK7(sK6,sK5)
| vf(sK6,sK1) = sF52
| vf(sK5,sK1) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(forward_subsumption_resolution,[],[f11113,f707]) ).
fof(f11137,plain,
( sK1 = sK6
| vf(sK5,sK6) != sK7(sK6,sK5)
| vf(sK6,sK1) = sF52
| vf(sK5,sK1) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(forward_subsumption_resolution,[],[f11125,f706]) ).
fof(f11149,plain,
( vf(sK5,sK6) != sK7(sK6,sK5)
| vf(sK6,sK1) = sF52
| vf(sK5,sK1) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(forward_subsumption_resolution,[],[f11137,f708]) ).
fof(f11161,plain,
( vf(sK6,sK5) != sK7(sK6,sK5)
| vf(sK6,sK1) = sF52
| vf(sK5,sK1) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(forward_demodulation,[],[f11149,f1941]) ).
fof(f11173,plain,
( vf(sK6,sK1) = sF52
| vf(sK5,sK1) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(forward_subsumption_resolution,[],[f11161,f2850]) ).
fof(f11178,plain,
( sF52 = sF53
| vf(sK5,sK1) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(forward_demodulation,[],[f11173,f1501]) ).
fof(f11182,plain,
( vf(sK5,sK1) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(forward_subsumption_resolution,[],[f11178,f1502]) ).
fof(f11186,plain,
( vf(sK1,sK5) != sK7(sK1,sK5)
| ~ spl54_588 ),
inference(forward_demodulation,[],[f11182,f1975]) ).
fof(f11202,plain,
( $false
| ~ spl54_588 ),
inference(forward_subsumption_resolution,[],[f11186,f2857]) ).
fof(f11203,plain,
~ spl54_588,
inference(avatar_contradiction_clause,[],[f11202]) ).
fof(f11223,plain,
( vangle(sK6,sK1,sK5) != vangle(sK6,sK1,sK5)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| vd1371 = sK1
| sK1 = sK5
| vd1371 = sK5
| vf(sK1,vd1371) != sK7(sK6,sK5)
| vf(vd1371,sK5) = sF53
| vf(sK1,sK5) != sK7(sK1,sK5)
| ~ spl54_591 ),
inference(superposition,[],[f10263,f1553]) ).
fof(f11242,plain,
( ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| vd1371 = sK1
| sK1 = sK5
| vd1371 = sK5
| vf(sK1,vd1371) != sK7(sK6,sK5)
| vf(vd1371,sK5) = sF53
| vf(sK1,sK5) != sK7(sK1,sK5)
| ~ spl54_591 ),
inference(trivial_inequality_removal,[],[f11223]) ).
fof(f11254,plain,
( ~ rpoint(vd1371)
| ~ rpoint(sK5)
| vd1371 = sK1
| sK1 = sK5
| vd1371 = sK5
| vf(sK1,vd1371) != sK7(sK6,sK5)
| vf(vd1371,sK5) = sF53
| vf(sK1,sK5) != sK7(sK1,sK5)
| ~ spl54_591 ),
inference(forward_subsumption_resolution,[],[f11242,f439]) ).
fof(f11266,plain,
( ~ rpoint(sK5)
| vd1371 = sK1
| sK1 = sK5
| vd1371 = sK5
| vf(sK1,vd1371) != sK7(sK6,sK5)
| vf(vd1371,sK5) = sF53
| vf(sK1,sK5) != sK7(sK1,sK5)
| ~ spl54_591 ),
inference(forward_subsumption_resolution,[],[f11254,f438]) ).
fof(f11278,plain,
( vd1371 = sK1
| sK1 = sK5
| vd1371 = sK5
| vf(sK1,vd1371) != sK7(sK6,sK5)
| vf(vd1371,sK5) = sF53
| vf(sK1,sK5) != sK7(sK1,sK5)
| ~ spl54_591 ),
inference(forward_subsumption_resolution,[],[f11266,f460]) ).
fof(f11290,plain,
( sK1 = sK5
| vd1371 = sK5
| vf(sK1,vd1371) != sK7(sK6,sK5)
| vf(vd1371,sK5) = sF53
| vf(sK1,sK5) != sK7(sK1,sK5)
| spl54_13
| ~ spl54_591 ),
inference(forward_subsumption_resolution,[],[f11278,f1578]) ).
fof(f11302,plain,
( vd1371 = sK5
| vf(sK1,vd1371) != sK7(sK6,sK5)
| vf(vd1371,sK5) = sF53
| vf(sK1,sK5) != sK7(sK1,sK5)
| spl54_13
| ~ spl54_591 ),
inference(forward_subsumption_resolution,[],[f11290,f706]) ).
fof(f11314,plain,
( vf(sK1,vd1371) != sK7(sK6,sK5)
| vf(vd1371,sK5) = sF53
| vf(sK1,sK5) != sK7(sK1,sK5)
| spl54_13
| spl54_15
| ~ spl54_591 ),
inference(forward_subsumption_resolution,[],[f11302,f1588]) ).
fof(f11326,plain,
( vf(sK1,vd1371) != sK7(sK6,sK5)
| vf(vd1371,sK5) = sF53
| spl54_13
| spl54_15
| ~ spl54_591 ),
inference(forward_subsumption_resolution,[],[f11314,f2857]) ).
fof(f11330,plain,
( vf(sK6,sK5) != sK7(sK6,sK5)
| vf(vd1371,sK5) = sF53
| spl54_13
| spl54_15
| ~ spl54_591 ),
inference(forward_demodulation,[],[f11326,f701]) ).
fof(f11333,plain,
( vf(vd1371,sK5) = sF53
| spl54_13
| spl54_15
| ~ spl54_591 ),
inference(forward_subsumption_resolution,[],[f11330,f2850]) ).
fof(f11336,plain,
( sF52 = sF53
| spl54_13
| spl54_15
| ~ spl54_591 ),
inference(forward_demodulation,[],[f11333,f1499]) ).
fof(f11338,plain,
( $false
| spl54_13
| spl54_15
| ~ spl54_591 ),
inference(forward_subsumption_resolution,[],[f11336,f1502]) ).
fof(f11339,plain,
( spl54_13
| spl54_15
| ~ spl54_591 ),
inference(avatar_contradiction_clause,[],[f11338]) ).
fof(f11353,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| ~ rpoint(sK5)
| ~ rpoint(vd1371)
| ~ rpoint(sK1)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(superposition,[],[f785,f1553]) ).
fof(f11464,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| ~ rpoint(vd1371)
| ~ rpoint(sK1)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f11353,f460]) ).
fof(f11510,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| ~ rpoint(sK1)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f11464,f438]) ).
fof(f11556,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f11510,f439]) ).
fof(f11602,plain,
! [X2,X0,X1] :
( vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK1,vd1371,sK5))
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f11556,f1499]) ).
fof(f11647,plain,
! [X2,X0,X1] :
( vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK1,vd1371,sK5))
| vf(X1,X0) != vf(sK1,vd1371)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f11602,f2857]) ).
fof(f11689,plain,
! [X2,X0,X1] :
( vf(X1,X0) != vf(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK1,vd1371,sK5))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f11647,f701]) ).
fof(f11728,plain,
! [X2,X0,X1] :
( vf(X1,X0) != sK7(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| ron(sK1,sK4(sK1,vd1371,sK5))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f11689,f2850]) ).
fof(f11757,definition,
( spl54_671
<=> ron(sK1,sK4(sK1,vd1371,sK5)) ),
introduced(definition,[new_symbols(definition,[spl54_671])],[avatar_definition]) ).
fof(f11759,plain,
( ron(sK1,sK4(sK1,vd1371,sK5))
| ~ spl54_671 ),
inference(avatar_component_clause,[],[f11757]) ).
fof(f11760,plain,
( spl54_671
| spl54_588 ),
inference(avatar_split_clause,[],[f11728,f10234,f11757]) ).
fof(f13389,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| ~ rpoint(sK5)
| ~ rpoint(vd1371)
| ~ rpoint(sK1)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(superposition,[],[f791,f1553]) ).
fof(f13417,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK5,sK6,sK1))
| vf(X0,X2) = vf(sK6,sK1)
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(superposition,[],[f791,f705]) ).
fof(f13874,plain,
! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ~ rR(sK5,sK6,sK1)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f2371,f706]) ).
fof(f13875,plain,
! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ron(sK1,X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| sK5 = sK6
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f2437,f706]) ).
fof(f13882,plain,
( ! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ron(vd1371,X0)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| sK1 = sK5
| ~ rline(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK1) )
| spl54_13
| spl54_15 ),
inference(forward_subsumption_resolution,[],[f2536,f1578]) ).
fof(f13883,plain,
! [X2,X3,X0,X1] :
( ~ ron(X2,sK10(X0,X3))
| rR(X2,X0,X1)
| rR(X0,X1,X2)
| ~ ron(X1,sK10(X0,X3))
| rR(X1,X0,X2)
| X1 = X2
| X0 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X3
| ~ rpoint(X3) ),
inference(forward_subsumption_resolution,[],[f4005,f962]) ).
fof(f13891,plain,
! [X0] :
( ~ ron(vd1371,X0)
| ~ ron(sK6,X0)
| ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f4803,f439]) ).
fof(f13892,plain,
! [X0] :
( ~ ron(vd1371,X0)
| ~ ron(sK1,X0)
| ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f4802,f462]) ).
fof(f13943,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK5,sK6,sK1))
| vf(X0,X2) = vf(sK6,sK1)
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f13417,f439]) ).
fof(f13971,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| ~ rpoint(vd1371)
| ~ rpoint(sK1)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f13389,f460]) ).
fof(f13986,plain,
! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ~ rR(sK5,sK6,sK1)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f13874,f707]) ).
fof(f13987,plain,
! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ron(sK1,X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f13875,f707]) ).
fof(f13994,plain,
( ! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ron(vd1371,X0)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK1) )
| spl54_13
| spl54_15 ),
inference(forward_subsumption_resolution,[],[f13882,f706]) ).
fof(f13997,plain,
! [X0] :
( ~ ron(vd1371,X0)
| ~ ron(sK6,X0)
| ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f13891,f438]) ).
fof(f13998,plain,
! [X0] :
( ~ ron(vd1371,X0)
| ~ ron(sK1,X0)
| ron(sK6,X0)
| ~ rline(X0)
| ~ rpoint(sK1) ),
inference(forward_subsumption_resolution,[],[f13892,f438]) ).
fof(f14011,definition,
( spl54_803
<=> rline(sK4(sK1,vd1371,sK5)) ),
introduced(definition,[new_symbols(definition,[spl54_803])],[avatar_definition]) ).
fof(f14012,plain,
( rline(sK4(sK1,vd1371,sK5))
| ~ spl54_803 ),
inference(avatar_component_clause,[],[f14011]) ).
fof(f14031,definition,
( spl54_808
<=> rline(sK4(sK5,sK6,sK1)) ),
introduced(definition,[new_symbols(definition,[spl54_808])],[avatar_definition]) ).
fof(f14032,plain,
( rline(sK4(sK5,sK6,sK1))
| ~ spl54_808 ),
inference(avatar_component_clause,[],[f14031]) ).
fof(f14153,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK5,sK6,sK1))
| vf(X0,X2) = vf(sK6,sK1)
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| ~ rpoint(sK5)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f13943,f462]) ).
fof(f14181,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| ~ rpoint(sK1)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f13971,f438]) ).
fof(f14196,plain,
! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ~ rR(sK5,sK6,sK1)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f13986,f439]) ).
fof(f14197,plain,
! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ron(sK1,X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f13987,f439]) ).
fof(f14204,plain,
( ! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ron(vd1371,X0)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK1) )
| spl54_13
| spl54_15 ),
inference(forward_subsumption_resolution,[],[f13994,f438]) ).
fof(f14207,plain,
! [X0] :
( ~ ron(sK6,X0)
| ~ ron(vd1371,X0)
| ron(sK1,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f13997,f462]) ).
fof(f14208,plain,
! [X0] :
( ~ ron(sK1,X0)
| ~ ron(vd1371,X0)
| ron(sK6,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f13998,f439]) ).
fof(f14223,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK5,sK6,sK1))
| vf(X0,X2) = vf(sK6,sK1)
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f14153,f460]) ).
fof(f14251,plain,
! [X2,X0,X1] :
( vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK1,vd1371,sK5))
| vf(X0,X2) = vf(vd1371,sK5)
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f14181,f439]) ).
fof(f14266,plain,
! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ~ rR(sK5,sK6,sK1)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f14196,f462]) ).
fof(f14267,plain,
! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ron(sK1,X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ rline(X0)
| ~ rpoint(sK5) ),
inference(forward_subsumption_resolution,[],[f14197,f462]) ).
fof(f14274,plain,
( ! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ron(vd1371,X0)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK1) )
| spl54_13
| spl54_15 ),
inference(forward_subsumption_resolution,[],[f14204,f460]) ).
fof(f14284,plain,
! [X2,X0,X1] :
( vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK5,sK6,sK1))
| vf(X1,X2) != vf(sK5,sK1)
| vf(X1,X0) != vf(sK5,sK6)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f14223,f1501]) ).
fof(f14312,plain,
! [X2,X0,X1] :
( vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK1,vd1371,sK5))
| vf(X1,X2) != vf(sK1,sK5)
| vf(X1,X0) != vf(sK1,vd1371)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f14251,f1499]) ).
fof(f14326,plain,
! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ~ rR(sK5,sK6,sK1)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f14266,f460]) ).
fof(f14327,plain,
! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ron(sK1,X0)
| ~ ron(sK6,X0)
| ~ ron(sK5,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f14267,f460]) ).
fof(f14334,plain,
( ! [X0] :
( vd684 != vangle(sK6,sK1,sK5)
| ron(vd1371,X0)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| ~ rline(X0) )
| spl54_13
| spl54_15 ),
inference(forward_subsumption_resolution,[],[f14274,f439]) ).
fof(f14344,plain,
! [X2,X0,X1] :
( vf(X1,X2) != vf(sK1,sK5)
| vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK5,sK6,sK1))
| vf(X1,X0) != vf(sK5,sK6)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f14284,f1975]) ).
fof(f14371,plain,
! [X2,X0,X1] :
( vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK1,vd1371,sK5))
| vf(X1,X0) != vf(sK1,vd1371)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f14312,f2857]) ).
fof(f14381,definition,
( spl54_838
<=> ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_838])],[avatar_definition]) ).
fof(f14382,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(sK5,X0) )
| ~ spl54_838 ),
inference(avatar_component_clause,[],[f14381]) ).
fof(f14384,definition,
( spl54_839
<=> rR(sK5,sK6,sK1) ),
introduced(definition,[new_symbols(definition,[spl54_839])],[avatar_definition]) ).
fof(f14385,plain,
( rR(sK5,sK6,sK1)
| ~ spl54_839 ),
inference(avatar_component_clause,[],[f14384]) ).
fof(f14386,plain,
( ~ rR(sK5,sK6,sK1)
| spl54_839 ),
inference(avatar_component_clause,[],[f14384]) ).
fof(f14388,definition,
( spl54_840
<=> vd684 = vangle(sK6,sK1,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_840])],[avatar_definition]) ).
fof(f14389,plain,
( vd684 = vangle(sK6,sK1,sK5)
| ~ spl54_840 ),
inference(avatar_component_clause,[],[f14388]) ).
fof(f14390,plain,
( vd684 != vangle(sK6,sK1,sK5)
| spl54_840 ),
inference(avatar_component_clause,[],[f14388]) ).
fof(f14391,plain,
( spl54_838
| ~ spl54_839
| ~ spl54_840 ),
inference(avatar_split_clause,[],[f14326,f14388,f14384,f14381]) ).
fof(f14393,definition,
( spl54_841
<=> ! [X0] :
( ron(sK1,X0)
| ~ rline(X0)
| ~ ron(sK5,X0)
| ~ ron(sK6,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_841])],[avatar_definition]) ).
fof(f14394,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(sK5,X0)
| ron(sK1,X0) )
| ~ spl54_841 ),
inference(avatar_component_clause,[],[f14393]) ).
fof(f14395,plain,
( spl54_841
| ~ spl54_840 ),
inference(avatar_split_clause,[],[f14327,f14388,f14393]) ).
fof(f14401,definition,
( spl54_843
<=> ! [X0] :
( ~ ron(sK1,X0)
| ~ rline(X0)
| ~ ron(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_843])],[avatar_definition]) ).
fof(f14402,plain,
( ! [X0] :
( ~ ron(sK1,X0)
| ~ rline(X0)
| ~ ron(sK5,X0) )
| ~ spl54_843 ),
inference(avatar_component_clause,[],[f14401]) ).
fof(f14404,definition,
( spl54_844
<=> rR(sK5,sK1,sK6) ),
introduced(definition,[new_symbols(definition,[spl54_844])],[avatar_definition]) ).
fof(f14405,plain,
( rR(sK5,sK1,sK6)
| ~ spl54_844 ),
inference(avatar_component_clause,[],[f14404]) ).
fof(f14406,plain,
( ~ rR(sK5,sK1,sK6)
| spl54_844 ),
inference(avatar_component_clause,[],[f14404]) ).
fof(f14424,definition,
( spl54_848
<=> ! [X0] :
( ron(vd1371,X0)
| ~ rline(X0)
| ~ ron(sK1,X0)
| ~ ron(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_848])],[avatar_definition]) ).
fof(f14425,plain,
( ! [X0] :
( ~ ron(sK5,X0)
| ~ rline(X0)
| ~ ron(sK1,X0)
| ron(vd1371,X0) )
| ~ spl54_848 ),
inference(avatar_component_clause,[],[f14424]) ).
fof(f14426,plain,
( spl54_848
| ~ spl54_840
| spl54_13
| spl54_15 ),
inference(avatar_split_clause,[],[f14334,f1587,f1577,f14388,f14424]) ).
fof(f14465,plain,
! [X2,X0,X1] :
( vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK5,sK6,sK1))
| vf(X1,X0) != vf(sK5,sK6)
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f14344,f2857]) ).
fof(f14489,plain,
! [X2,X0,X1] :
( vf(X1,X0) != vf(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK1,vd1371,sK5))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f14371,f701]) ).
fof(f14500,plain,
! [X2,X0,X1] :
( vf(X1,X0) != vf(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK5,sK6,sK1))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f14465,f1941]) ).
fof(f14517,plain,
! [X2,X0,X1] :
( vf(X1,X0) != sK7(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF52
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK1,vd1371,sK5))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f14489,f2850]) ).
fof(f14520,plain,
! [X2,X0,X1] :
( vf(X1,X0) != sK7(sK6,sK5)
| vf(X1,X2) != sK7(sK1,sK5)
| vf(X0,X2) = sF53
| vangle(X0,X1,X2) != vangle(sK6,sK1,sK5)
| rline(sK4(sK5,sK6,sK1))
| X0 = X2
| X1 = X2
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_demodulation,[],[f14500,f2850]) ).
fof(f14532,plain,
( spl54_803
| spl54_588 ),
inference(avatar_split_clause,[],[f14517,f10234,f14011]) ).
fof(f14533,plain,
( spl54_808
| spl54_591 ),
inference(avatar_split_clause,[],[f14520,f10262,f14031]) ).
fof(f14561,plain,
! [X2,X0,X1] :
( rR(X0,X1,X2)
| rR(X1,X2,X0)
| ~ ron(X2,sK10(X1,X0))
| rR(X2,X1,X0)
| X0 = X2
| X0 = X1
| X1 = X2
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(X1)
| X0 = X1
| ~ rpoint(X0)
| X0 = X1
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f13883,f958]) ).
fof(f14565,plain,
! [X2,X0,X1] :
( ~ ron(X2,sK10(X1,X0))
| rR(X1,X2,X0)
| rR(X0,X1,X2)
| rR(X2,X1,X0)
| X0 = X2
| X0 = X1
| X1 = X2
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(duplicate_literal_removal,[],[f14561]) ).
fof(f14574,plain,
! [X2,X3,X0,X1,X4,X5] :
( rR(X0,X1,X2)
| X0 = X3
| X0 = X2
| X0 = X4
| X0 = X1
| ~ ron(X3,X5)
| ~ ron(X4,X5)
| rR(X0,X4,X3)
| ~ ron(X1,sK10(X2,X0))
| vangle(X2,X0,X3) = vangle(X1,X0,X4)
| ~ rline(X5)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X2
| ~ rpoint(X2)
| X0 = X2
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(resolution,[],[f2191,f960]) ).
fof(f14576,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ ron(X1,sK10(X2,X0))
| X0 = X3
| X0 = X2
| X0 = X4
| X0 = X1
| ~ ron(X3,X5)
| ~ ron(X4,X5)
| rR(X0,X4,X3)
| rR(X0,X1,X2)
| vangle(X2,X0,X3) = vangle(X1,X0,X4)
| ~ rline(X5)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(duplicate_literal_removal,[],[f14574]) ).
fof(f14580,plain,
! [X2,X3,X0,X1,X4] :
( X0 = X1
| X0 = X2
| X0 = X3
| X0 = X2
| ~ ron(X1,X4)
| ~ ron(X3,X4)
| rR(X0,X3,X1)
| rR(X0,X2,X2)
| vangle(X2,X0,X1) = vangle(X2,X0,X3)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X0)
| X0 = X2
| ~ rpoint(X0)
| ~ rpoint(X2) ),
inference(resolution,[],[f14576,f960]) ).
fof(f14582,plain,
! [X2,X3,X0,X1,X4] :
( X0 = X1
| X0 = X2
| X0 = X3
| ~ ron(X1,X4)
| ~ ron(X3,X4)
| rR(X0,X3,X1)
| rR(X0,X2,X2)
| vangle(X2,X0,X1) = vangle(X2,X0,X3)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X0) ),
inference(duplicate_literal_removal,[],[f14580]) ).
fof(f14585,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,X4)
| X0 = X2
| X0 = X3
| ~ ron(X1,X4)
| X0 = X1
| rR(X0,X3,X1)
| vangle(X2,X0,X1) = vangle(X2,X0,X3)
| ~ rline(X4)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f14582,f1504]) ).
fof(f14586,plain,
! [X2,X3,X0,X1,X4] :
( X0 = X1
| X0 = X2
| ~ ron(X3,sK10(X4,X2))
| X0 = X3
| rR(X0,X2,X3)
| vangle(X1,X0,X2) = vangle(X1,X0,X3)
| ~ rline(sK10(X4,X2))
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| X2 = X4
| ~ rpoint(X2)
| ~ rpoint(X4) ),
inference(resolution,[],[f14585,f958]) ).
fof(f14600,plain,
! [X2,X3,X0,X1,X4] :
( X0 = X1
| X0 = X2
| ~ ron(X3,sK10(X4,X2))
| X0 = X3
| rR(X0,X2,X3)
| vangle(X1,X0,X2) = vangle(X1,X0,X3)
| ~ rline(sK10(X4,X2))
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| X2 = X4
| ~ rpoint(X4) ),
inference(duplicate_literal_removal,[],[f14586]) ).
fof(f14611,plain,
! [X2,X3,X0,X1,X4] :
( ~ ron(X3,sK10(X4,X2))
| X0 = X2
| X0 = X1
| X0 = X3
| rR(X0,X2,X3)
| vangle(X1,X0,X2) = vangle(X1,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| X2 = X4
| ~ rpoint(X4) ),
inference(forward_subsumption_resolution,[],[f14600,f962]) ).
fof(f14633,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| X0 = X2
| X0 = X3
| rR(X0,X1,X3)
| vangle(X2,X0,X1) = vangle(X2,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| X1 = X3
| ~ rpoint(X3)
| X1 = X3
| ~ rpoint(X1)
| ~ rpoint(X3) ),
inference(resolution,[],[f14611,f960]) ).
fof(f14635,plain,
! [X2,X3,X0,X1] :
( ~ rpoint(X3)
| X0 = X2
| X0 = X3
| rR(X0,X1,X3)
| vangle(X2,X0,X1) = vangle(X2,X0,X3)
| X0 = X1
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| X1 = X3 ),
inference(duplicate_literal_removal,[],[f14633]) ).
fof(f14649,plain,
! [X2,X0,X1] :
( ~ rpoint(X2)
| sK1 = X0
| rR(X0,X2,sK1)
| vangle(X1,X0,X2) = vangle(X1,X0,sK1)
| X0 = X2
| ~ rpoint(X1)
| X0 = X1
| ~ rpoint(X0)
| sK1 = X2 ),
inference(resolution,[],[f14635,f439]) ).
fof(f14650,plain,
! [X2,X0,X1] :
( ~ rpoint(X2)
| sK5 = X0
| rR(X0,X2,sK5)
| vangle(X1,X0,X2) = vangle(X1,X0,sK5)
| X0 = X2
| ~ rpoint(X1)
| X0 = X1
| ~ rpoint(X0)
| sK5 = X2 ),
inference(resolution,[],[f14635,f460]) ).
fof(f14669,plain,
! [X0,X1] :
( sK1 = X0
| rR(X0,sK6,sK1)
| vangle(X1,X0,sK1) = vangle(X1,X0,sK6)
| sK6 = X0
| ~ rpoint(X1)
| X0 = X1
| ~ rpoint(X0)
| sK1 = sK6 ),
inference(resolution,[],[f14649,f462]) ).
fof(f14671,plain,
! [X0,X1] :
( ~ rpoint(X1)
| rR(X0,sK6,sK1)
| vangle(X1,X0,sK1) = vangle(X1,X0,sK6)
| sK6 = X0
| sK1 = X0
| X0 = X1
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f14669,f708]) ).
fof(f14700,plain,
! [X0,X1] :
( sK5 = X0
| rR(X0,sK6,sK5)
| vangle(X1,X0,sK5) = vangle(X1,X0,sK6)
| sK6 = X0
| ~ rpoint(X1)
| X0 = X1
| ~ rpoint(X0)
| sK5 = sK6 ),
inference(resolution,[],[f14650,f462]) ).
fof(f14702,plain,
! [X0,X1] :
( ~ rpoint(X1)
| rR(X0,sK6,sK5)
| vangle(X1,X0,sK5) = vangle(X1,X0,sK6)
| sK6 = X0
| sK5 = X0
| X0 = X1
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f14700,f707]) ).
fof(f14792,plain,
! [X0] :
( rR(X0,sK6,sK1)
| vangle(sK6,X0,sK1) = vangle(sK6,X0,sK6)
| sK6 = X0
| sK1 = X0
| sK6 = X0
| ~ rpoint(X0) ),
inference(resolution,[],[f14671,f462]) ).
fof(f14793,plain,
! [X0] :
( rR(X0,sK6,sK1)
| vangle(sK6,X0,sK1) = vangle(sK6,X0,sK6)
| sK6 = X0
| sK1 = X0
| ~ rpoint(X0) ),
inference(duplicate_literal_removal,[],[f14792]) ).
fof(f14844,plain,
! [X0] :
( rR(X0,sK6,sK5)
| vangle(sK6,X0,sK6) = vangle(sK6,X0,sK5)
| sK6 = X0
| sK5 = X0
| sK6 = X0
| ~ rpoint(X0) ),
inference(resolution,[],[f14702,f462]) ).
fof(f14845,plain,
! [X0] :
( rR(X0,sK6,sK5)
| vangle(sK6,X0,sK6) = vangle(sK6,X0,sK5)
| sK6 = X0
| sK5 = X0
| ~ rpoint(X0) ),
inference(duplicate_literal_removal,[],[f14844]) ).
fof(f14851,plain,
! [X0] :
( ~ ron(vd1371,sK10(sK6,X0))
| ron(sK1,sK10(sK6,X0))
| ~ rline(sK10(sK6,X0))
| sK6 = X0
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(resolution,[],[f14207,f960]) ).
fof(f14854,plain,
! [X0] :
( ~ ron(vd1371,sK10(sK6,X0))
| ron(sK1,sK10(sK6,X0))
| sK6 = X0
| ~ rpoint(X0)
| ~ rpoint(sK6) ),
inference(forward_subsumption_resolution,[],[f14851,f962]) ).
fof(f14856,plain,
! [X0] :
( ~ ron(vd1371,sK10(sK6,X0))
| ron(sK1,sK10(sK6,X0))
| sK6 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[],[f14854,f462]) ).
fof(f15182,plain,
( ron(sK1,sK10(sK6,vd1371))
| vd1371 = sK6
| ~ rpoint(vd1371)
| vd1371 = sK6
| ~ rpoint(vd1371)
| ~ rpoint(sK6) ),
inference(resolution,[],[f14856,f958]) ).
fof(f15183,plain,
( ron(sK1,sK10(sK6,vd1371))
| vd1371 = sK6
| ~ rpoint(vd1371)
| ~ rpoint(sK6) ),
inference(duplicate_literal_removal,[],[f15182]) ).
fof(f15184,plain,
( ron(sK1,sK10(sK6,vd1371))
| ~ rpoint(vd1371)
| ~ rpoint(sK6)
| spl54_73 ),
inference(forward_subsumption_resolution,[],[f15183,f2175]) ).
fof(f15185,plain,
( ron(sK1,sK10(sK6,vd1371))
| ~ rpoint(sK6)
| spl54_73 ),
inference(forward_subsumption_resolution,[],[f15184,f438]) ).
fof(f15186,plain,
( ron(sK1,sK10(sK6,vd1371))
| spl54_73 ),
inference(forward_subsumption_resolution,[],[f15185,f462]) ).
fof(f15360,definition,
( spl54_873
<=> ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(sK1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl54_873])],[avatar_definition]) ).
fof(f15361,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ rline(X0)
| ~ ron(sK1,X0) )
| ~ spl54_873 ),
inference(avatar_component_clause,[],[f15360]) ).
fof(f15418,plain,
( ~ rR(sK1,vd1371,sK6)
| ~ rpoint(sK1)
| ~ rpoint(vd1371) ),
inference(forward_subsumption_resolution,[],[f2419,f462]) ).
fof(f15423,plain,
( ~ rR(sK1,vd1371,sK6)
| ~ rpoint(vd1371) ),
inference(forward_subsumption_resolution,[],[f15418,f439]) ).
fof(f15428,plain,
~ rR(sK1,vd1371,sK6),
inference(forward_subsumption_resolution,[],[f15423,f438]) ).
fof(f15439,plain,
( ~ rline(sK4(sK5,sK6,sK1))
| ~ ron(sK1,sK4(sK5,sK6,sK1))
| ~ spl54_657
| ~ spl54_873 ),
inference(resolution,[],[f15361,f11025]) ).
fof(f15446,plain,
( ~ ron(sK1,sK4(sK5,sK6,sK1))
| ~ spl54_657
| ~ spl54_808
| ~ spl54_873 ),
inference(forward_subsumption_resolution,[],[f15439,f14032]) ).
fof(f15449,plain,
( $false
| ~ spl54_590
| ~ spl54_657
| ~ spl54_808
| ~ spl54_873 ),
inference(forward_subsumption_resolution,[],[f15446,f10260]) ).
fof(f15450,plain,
( ~ spl54_590
| ~ spl54_657
| ~ spl54_808
| ~ spl54_873 ),
inference(avatar_contradiction_clause,[],[f15449]) ).
fof(f15740,plain,
( ~ ron(vd1371,sK4(sK1,vd1371,sK5))
| ron(sK6,sK4(sK1,vd1371,sK5))
| ~ rline(sK4(sK1,vd1371,sK5))
| ~ spl54_671 ),
inference(resolution,[],[f14208,f11759]) ).
fof(f15750,plain,
( ron(sK6,sK4(sK1,vd1371,sK5))
| ~ rline(sK4(sK1,vd1371,sK5))
| ~ spl54_656
| ~ spl54_671 ),
inference(forward_subsumption_resolution,[],[f15740,f11006]) ).
fof(f15754,plain,
( ron(sK6,sK4(sK1,vd1371,sK5))
| ~ spl54_656
| ~ spl54_671
| ~ spl54_803 ),
inference(forward_subsumption_resolution,[],[f15750,f14012]) ).
fof(f16230,definition,
( spl54_911
<=> rR(sK1,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_911])],[avatar_definition]) ).
fof(f16231,plain,
( ~ rR(sK1,sK6,sK5)
| spl54_911 ),
inference(avatar_component_clause,[],[f16230]) ).
fof(f16232,plain,
( rR(sK1,sK6,sK5)
| ~ spl54_911 ),
inference(avatar_component_clause,[],[f16230]) ).
fof(f16241,plain,
( rR(sK1,sK5,sK6)
| ~ rpoint(sK5)
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ spl54_911 ),
inference(resolution,[],[f16232,f898]) ).
fof(f16250,plain,
( rR(sK1,sK5,sK6)
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ spl54_911 ),
inference(forward_subsumption_resolution,[],[f16241,f460]) ).
fof(f16258,plain,
( rR(sK1,sK5,sK6)
| ~ rpoint(sK6)
| ~ spl54_911 ),
inference(forward_subsumption_resolution,[],[f16250,f439]) ).
fof(f16266,plain,
( rR(sK1,sK5,sK6)
| ~ spl54_911 ),
inference(forward_subsumption_resolution,[],[f16258,f462]) ).
fof(f16339,plain,
( ! [X0] :
( ~ rline(sK10(X0,sK6))
| ~ ron(sK5,sK10(X0,sK6))
| ron(sK1,sK10(X0,sK6))
| sK6 = X0
| ~ rpoint(sK6)
| ~ rpoint(X0) )
| ~ spl54_841 ),
inference(resolution,[],[f14394,f958]) ).
fof(f16344,plain,
( ! [X0] :
( ~ ron(sK5,sK10(X0,sK6))
| ron(sK1,sK10(X0,sK6))
| sK6 = X0
| ~ rpoint(sK6)
| ~ rpoint(X0) )
| ~ spl54_841 ),
inference(forward_subsumption_resolution,[],[f16339,f962]) ).
fof(f16346,plain,
( ! [X0] :
( ~ ron(sK5,sK10(X0,sK6))
| ron(sK1,sK10(X0,sK6))
| sK6 = X0
| ~ rpoint(X0) )
| ~ spl54_841 ),
inference(forward_subsumption_resolution,[],[f16344,f462]) ).
fof(f16414,plain,
( vangle(sK6,sK5,sK1) = vangle(sK6,sK5,sK6)
| sK5 = sK6
| sK1 = sK5
| ~ rpoint(sK5)
| spl54_839 ),
inference(resolution,[],[f14386,f14793]) ).
fof(f16417,plain,
( vangle(sK6,sK5,sK1) = vangle(sK6,sK5,sK6)
| sK1 = sK5
| ~ rpoint(sK5)
| spl54_839 ),
inference(forward_subsumption_resolution,[],[f16414,f707]) ).
fof(f16419,plain,
( vangle(sK6,sK5,sK1) = vangle(sK6,sK5,sK6)
| ~ rpoint(sK5)
| spl54_839 ),
inference(forward_subsumption_resolution,[],[f16417,f706]) ).
fof(f16421,plain,
( vangle(sK6,sK5,sK1) = vangle(sK6,sK5,sK6)
| spl54_839 ),
inference(forward_subsumption_resolution,[],[f16419,f460]) ).
fof(f16423,plain,
( vd684 = vangle(sK6,sK5,sK1)
| spl54_839 ),
inference(forward_demodulation,[],[f16421,f2159]) ).
fof(f16425,plain,
( vd684 = vangle(sK6,sK1,sK5)
| spl54_839 ),
inference(forward_demodulation,[],[f16423,f705]) ).
fof(f16428,plain,
( $false
| spl54_839
| spl54_840 ),
inference(forward_subsumption_resolution,[],[f16425,f14390]) ).
fof(f16429,plain,
( spl54_839
| spl54_840 ),
inference(avatar_contradiction_clause,[],[f16428]) ).
fof(f16432,plain,
( ~ rR(sK1,sK5,sK6)
| ~ rpoint(sK6)
| ~ rpoint(sK1)
| ~ rpoint(sK5)
| ~ spl54_844 ),
inference(resolution,[],[f14405,f887]) ).
fof(f16433,plain,
( rR(sK5,sK6,sK1)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(sK1)
| ~ spl54_844 ),
inference(resolution,[],[f14405,f898]) ).
fof(f16441,plain,
( ~ rR(sK1,sK5,sK6)
| ~ rpoint(sK1)
| ~ rpoint(sK5)
| ~ spl54_844 ),
inference(forward_subsumption_resolution,[],[f16432,f462]) ).
fof(f16447,plain,
( ~ rR(sK1,sK5,sK6)
| ~ rpoint(sK5)
| ~ spl54_844 ),
inference(forward_subsumption_resolution,[],[f16441,f439]) ).
fof(f16453,plain,
( ~ rR(sK1,sK5,sK6)
| ~ spl54_844 ),
inference(forward_subsumption_resolution,[],[f16447,f460]) ).
fof(f16577,plain,
( ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ rpoint(sK1)
| spl54_839
| ~ spl54_844 ),
inference(forward_subsumption_resolution,[],[f16433,f14386]) ).
fof(f16579,plain,
( ~ rpoint(sK5)
| ~ rpoint(sK1)
| spl54_839
| ~ spl54_844 ),
inference(forward_subsumption_resolution,[],[f16577,f462]) ).
fof(f16581,plain,
( ~ rpoint(sK1)
| spl54_839
| ~ spl54_844 ),
inference(forward_subsumption_resolution,[],[f16579,f460]) ).
fof(f16583,plain,
( $false
| spl54_839
| ~ spl54_844 ),
inference(forward_subsumption_resolution,[],[f16581,f439]) ).
fof(f16584,plain,
( spl54_839
| ~ spl54_844 ),
inference(avatar_contradiction_clause,[],[f16583]) ).
fof(f16588,definition,
( spl54_918
<=> rR(sK1,vd1371,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_918])],[avatar_definition]) ).
fof(f16589,plain,
( rR(sK1,vd1371,sK5)
| ~ spl54_918 ),
inference(avatar_component_clause,[],[f16588]) ).
fof(f16590,plain,
( ~ rR(sK1,vd1371,sK5)
| spl54_918 ),
inference(avatar_component_clause,[],[f16588]) ).
fof(f16601,plain,
( ! [X0] :
( vd684 != vd684
| ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| sK1 = sK5
| sK1 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK1) )
| ~ spl54_840 ),
inference(superposition,[],[f845,f14389]) ).
fof(f16602,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| sK1 = sK5
| sK1 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK1) )
| ~ spl54_840 ),
inference(trivial_inequality_removal,[],[f16601]) ).
fof(f16604,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| sK1 = sK5
| sK1 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK1) )
| ~ spl54_840
| ~ spl54_843 ),
inference(forward_subsumption_resolution,[],[f16602,f14402]) ).
fof(f16613,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| sK1 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK1) )
| ~ spl54_840
| ~ spl54_843 ),
inference(forward_subsumption_resolution,[],[f16604,f706]) ).
fof(f16622,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK1) )
| ~ spl54_840
| ~ spl54_843 ),
inference(forward_subsumption_resolution,[],[f16613,f708]) ).
fof(f16631,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK1) )
| ~ spl54_840
| ~ spl54_843 ),
inference(forward_subsumption_resolution,[],[f16622,f460]) ).
fof(f16640,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK1) )
| ~ spl54_840
| ~ spl54_843 ),
inference(forward_subsumption_resolution,[],[f16631,f462]) ).
fof(f16649,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| ~ rline(X0) )
| ~ spl54_840
| ~ spl54_843 ),
inference(forward_subsumption_resolution,[],[f16640,f439]) ).
fof(f16658,plain,
( spl54_873
| ~ spl54_840
| ~ spl54_843 ),
inference(avatar_split_clause,[],[f16649,f14401,f14388,f15360]) ).
fof(f16729,plain,
( rR(sK5,sK1,sK6)
| ~ rpoint(sK1)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ spl54_839 ),
inference(resolution,[],[f14385,f898]) ).
fof(f16842,plain,
( vangle(sK6,sK1,sK5) = vangle(sK6,sK1,sK6)
| sK1 = sK6
| sK1 = sK5
| ~ rpoint(sK1)
| spl54_911 ),
inference(resolution,[],[f16231,f14845]) ).
fof(f16843,plain,
( vangle(sK6,sK1,sK5) = vangle(sK6,sK1,sK6)
| sK1 = sK5
| ~ rpoint(sK1)
| spl54_911 ),
inference(forward_subsumption_resolution,[],[f16842,f708]) ).
fof(f16845,plain,
( vangle(sK6,sK1,sK5) = vangle(sK6,sK1,sK6)
| ~ rpoint(sK1)
| spl54_911 ),
inference(forward_subsumption_resolution,[],[f16843,f706]) ).
fof(f16847,plain,
( vangle(sK6,sK1,sK5) = vangle(sK6,sK1,sK6)
| spl54_911 ),
inference(forward_subsumption_resolution,[],[f16845,f439]) ).
fof(f16849,plain,
( vd684 = vangle(sK6,sK1,sK5)
| spl54_911 ),
inference(forward_demodulation,[],[f16847,f2151]) ).
fof(f16851,plain,
( $false
| spl54_840
| spl54_911 ),
inference(forward_subsumption_resolution,[],[f16849,f14390]) ).
fof(f16852,plain,
( spl54_840
| spl54_911 ),
inference(avatar_contradiction_clause,[],[f16851]) ).
fof(f16856,plain,
( $false
| ~ spl54_844
| ~ spl54_911 ),
inference(forward_subsumption_resolution,[],[f16266,f16453]) ).
fof(f16857,plain,
( ~ spl54_844
| ~ spl54_911 ),
inference(avatar_contradiction_clause,[],[f16856]) ).
fof(f16859,plain,
( ~ rpoint(sK1)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ spl54_839
| spl54_844 ),
inference(forward_subsumption_resolution,[],[f16729,f14406]) ).
fof(f16863,plain,
( ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ spl54_839
| spl54_844 ),
inference(forward_subsumption_resolution,[],[f16859,f439]) ).
fof(f16867,plain,
( ~ rpoint(sK6)
| ~ spl54_839
| spl54_844 ),
inference(forward_subsumption_resolution,[],[f16863,f460]) ).
fof(f16870,plain,
( $false
| ~ spl54_839
| spl54_844 ),
inference(forward_subsumption_resolution,[],[f16867,f462]) ).
fof(f16871,plain,
( ~ spl54_839
| spl54_844 ),
inference(avatar_contradiction_clause,[],[f16870]) ).
fof(f16976,plain,
( rR(sK1,sK1,sK6)
| ~ spl54_13 ),
inference(superposition,[],[f702,f1579]) ).
fof(f17031,plain,
( ~ rR(sK1,sK1,sK6)
| ~ spl54_13 ),
inference(superposition,[],[f15428,f1579]) ).
fof(f17056,plain,
( $false
| ~ spl54_13 ),
inference(forward_subsumption_resolution,[],[f16976,f17031]) ).
fof(f17057,plain,
~ spl54_13,
inference(avatar_contradiction_clause,[],[f17056]) ).
fof(f17567,plain,
( ! [X0] :
( vd684 != vd684
| ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| sK1 = sK5
| sK1 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK1) )
| ~ spl54_840 ),
inference(superposition,[],[f845,f14389]) ).
fof(f17568,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| sK1 = sK5
| sK1 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK1) )
| ~ spl54_840 ),
inference(trivial_inequality_removal,[],[f17567]) ).
fof(f17636,plain,
( rR(sK5,sK6,sK1)
| ~ spl54_15 ),
inference(superposition,[],[f1558,f1589]) ).
fof(f17745,plain,
( ~ rline(sK4(sK1,vd1371,sK5))
| ~ ron(sK5,sK4(sK1,vd1371,sK5))
| ~ spl54_656
| ~ spl54_671
| ~ spl54_803
| ~ spl54_838 ),
inference(resolution,[],[f14382,f15754]) ).
fof(f17752,plain,
( ~ ron(sK5,sK4(sK1,vd1371,sK5))
| ~ spl54_656
| ~ spl54_671
| ~ spl54_803
| ~ spl54_838 ),
inference(forward_subsumption_resolution,[],[f17745,f14012]) ).
fof(f17755,plain,
( $false
| ~ spl54_587
| ~ spl54_656
| ~ spl54_671
| ~ spl54_803
| ~ spl54_838 ),
inference(forward_subsumption_resolution,[],[f17752,f10232]) ).
fof(f17756,plain,
( ~ spl54_587
| ~ spl54_656
| ~ spl54_671
| ~ spl54_803
| ~ spl54_838 ),
inference(avatar_contradiction_clause,[],[f17755]) ).
fof(f17759,plain,
( $false
| ~ spl54_15
| spl54_839 ),
inference(forward_subsumption_resolution,[],[f17636,f14386]) ).
fof(f17760,plain,
( ~ spl54_15
| spl54_839 ),
inference(avatar_contradiction_clause,[],[f17759]) ).
fof(f17766,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| sK1 = sK6
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK1) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f17568,f706]) ).
fof(f17780,plain,
( vangle(vd1371,sK1,sK5) = vangle(sK5,sK1,vd1371)
| spl54_15 ),
inference(forward_subsumption_resolution,[],[f2528,f1588]) ).
fof(f17847,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| ~ rpoint(sK1) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f17766,f708]) ).
fof(f17852,plain,
( vangle(sK6,sK1,sK5) = vangle(sK5,sK1,vd1371)
| spl54_15 ),
inference(forward_demodulation,[],[f17780,f1553]) ).
fof(f17893,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK6)
| ~ rpoint(sK1) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f17847,f460]) ).
fof(f17896,plain,
( vd684 = vangle(sK5,sK1,vd1371)
| spl54_15
| ~ spl54_840 ),
inference(forward_demodulation,[],[f17852,f14389]) ).
fof(f17925,plain,
( ! [X0] :
( ron(sK5,X0)
| ~ ron(sK6,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK1) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f17893,f462]) ).
fof(f17940,plain,
( ! [X0] :
( ~ ron(sK6,X0)
| ron(sK5,X0)
| ~ ron(sK1,X0)
| ~ rline(X0) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f17925,f439]) ).
fof(f18102,plain,
( ! [X0] :
( ron(sK5,sK10(X0,sK6))
| ~ ron(sK1,sK10(X0,sK6))
| ~ rline(sK10(X0,sK6))
| sK6 = X0
| ~ rpoint(sK6)
| ~ rpoint(X0) )
| ~ spl54_840 ),
inference(resolution,[],[f17940,f958]) ).
fof(f18103,plain,
( ! [X0] :
( ron(sK5,sK10(sK6,X0))
| ~ ron(sK1,sK10(sK6,X0))
| ~ rline(sK10(sK6,X0))
| sK6 = X0
| ~ rpoint(X0)
| ~ rpoint(sK6) )
| ~ spl54_840 ),
inference(resolution,[],[f17940,f960]) ).
fof(f18106,plain,
( ! [X0] :
( ron(sK5,sK10(sK6,X0))
| ~ ron(sK1,sK10(sK6,X0))
| sK6 = X0
| ~ rpoint(X0)
| ~ rpoint(sK6) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18103,f962]) ).
fof(f18107,plain,
( ! [X0] :
( ron(sK5,sK10(X0,sK6))
| ~ ron(sK1,sK10(X0,sK6))
| sK6 = X0
| ~ rpoint(sK6)
| ~ rpoint(X0) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18102,f962]) ).
fof(f18108,plain,
( ! [X0] :
( ~ ron(sK1,sK10(sK6,X0))
| ron(sK5,sK10(sK6,X0))
| sK6 = X0
| ~ rpoint(X0) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18106,f462]) ).
fof(f18109,plain,
( ! [X0] :
( ~ ron(sK1,sK10(X0,sK6))
| ron(sK5,sK10(X0,sK6))
| sK6 = X0
| ~ rpoint(X0) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18107,f462]) ).
fof(f18110,plain,
( ron(sK5,sK10(sK6,vd1371))
| vd1371 = sK6
| ~ rpoint(vd1371)
| spl54_73
| ~ spl54_840 ),
inference(resolution,[],[f18108,f15186]) ).
fof(f18114,plain,
( ron(sK5,sK10(sK6,vd1371))
| ~ rpoint(vd1371)
| spl54_73
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18110,f2175]) ).
fof(f18116,plain,
( ron(sK5,sK10(sK6,vd1371))
| spl54_73
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18114,f438]) ).
fof(f18229,plain,
( ron(sK5,sK10(sK1,sK6))
| sK1 = sK6
| ~ rpoint(sK1)
| sK1 = sK6
| ~ rpoint(sK6)
| ~ rpoint(sK1)
| ~ spl54_840 ),
inference(resolution,[],[f18109,f960]) ).
fof(f18230,plain,
( ron(sK5,sK10(sK1,sK6))
| sK1 = sK6
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ spl54_840 ),
inference(duplicate_literal_removal,[],[f18229]) ).
fof(f18231,plain,
( ron(sK5,sK10(sK1,sK6))
| ~ rpoint(sK1)
| ~ rpoint(sK6)
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18230,f708]) ).
fof(f18233,plain,
( ron(sK5,sK10(sK1,sK6))
| ~ rpoint(sK6)
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18231,f439]) ).
fof(f18235,plain,
( ron(sK5,sK10(sK1,sK6))
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18233,f462]) ).
fof(f18244,plain,
( ! [X0] :
( rR(sK5,sK1,X0)
| rR(sK1,X0,sK5)
| ~ ron(X0,sK10(sK1,sK6))
| rR(X0,sK1,sK5)
| sK5 = X0
| sK1 = sK5
| sK1 = X0
| ~ rpoint(sK5)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| sK1 = sK6
| ~ rpoint(sK6) )
| ~ spl54_840 ),
inference(resolution,[],[f18235,f13883]) ).
fof(f18263,plain,
( ! [X0] :
( rR(sK5,sK1,X0)
| rR(sK1,X0,sK5)
| ~ ron(X0,sK10(sK1,sK6))
| rR(X0,sK1,sK5)
| sK5 = X0
| sK1 = X0
| ~ rpoint(sK5)
| ~ rpoint(X0)
| ~ rpoint(sK1)
| sK1 = sK6
| ~ rpoint(sK6) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18244,f706]) ).
fof(f18271,definition,
( spl54_932
<=> ron(sK1,sK10(sK1,sK6)) ),
introduced(definition,[new_symbols(definition,[spl54_932])],[avatar_definition]) ).
fof(f18272,plain,
( ron(sK1,sK10(sK1,sK6))
| ~ spl54_932 ),
inference(avatar_component_clause,[],[f18271]) ).
fof(f18273,plain,
( ~ ron(sK1,sK10(sK1,sK6))
| spl54_932 ),
inference(avatar_component_clause,[],[f18271]) ).
fof(f18279,definition,
( spl54_934
<=> rline(sK10(sK1,sK6)) ),
introduced(definition,[new_symbols(definition,[spl54_934])],[avatar_definition]) ).
fof(f18280,plain,
( rline(sK10(sK1,sK6))
| ~ spl54_934 ),
inference(avatar_component_clause,[],[f18279]) ).
fof(f18281,plain,
( ~ rline(sK10(sK1,sK6))
| spl54_934 ),
inference(avatar_component_clause,[],[f18279]) ).
fof(f18304,plain,
( ! [X0] :
( rR(sK5,sK1,X0)
| rR(sK1,X0,sK5)
| ~ ron(X0,sK10(sK1,sK6))
| rR(X0,sK1,sK5)
| sK5 = X0
| sK1 = X0
| ~ rpoint(X0)
| ~ rpoint(sK1)
| sK1 = sK6
| ~ rpoint(sK6) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18263,f460]) ).
fof(f18312,plain,
( ! [X0] :
( rR(sK5,sK1,X0)
| rR(sK1,X0,sK5)
| ~ ron(X0,sK10(sK1,sK6))
| rR(X0,sK1,sK5)
| sK5 = X0
| sK1 = X0
| ~ rpoint(X0)
| sK1 = sK6
| ~ rpoint(sK6) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18304,f439]) ).
fof(f18320,plain,
( ! [X0] :
( rR(sK5,sK1,X0)
| rR(sK1,X0,sK5)
| ~ ron(X0,sK10(sK1,sK6))
| rR(X0,sK1,sK5)
| sK5 = X0
| sK1 = X0
| ~ rpoint(X0)
| ~ rpoint(sK6) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18312,f708]) ).
fof(f18328,plain,
( ! [X0] :
( ~ ron(X0,sK10(sK1,sK6))
| rR(sK1,X0,sK5)
| rR(sK5,sK1,X0)
| rR(X0,sK1,sK5)
| sK5 = X0
| sK1 = X0
| ~ rpoint(X0) )
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18320,f462]) ).
fof(f18348,plain,
( ! [X0] :
( vd684 != vd684
| ~ rR(sK1,sK5,vd1371)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| vd1371 = sK1
| sK1 = sK5
| ~ rline(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK1) )
| spl54_15
| ~ spl54_840 ),
inference(superposition,[],[f841,f17896]) ).
fof(f18351,plain,
( ! [X0] :
( ~ rR(sK1,sK5,vd1371)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| vd1371 = sK1
| sK1 = sK5
| ~ rline(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK1) )
| spl54_15
| ~ spl54_840 ),
inference(trivial_inequality_removal,[],[f18348]) ).
fof(f18501,plain,
( ron(sK1,sK10(sK1,sK6))
| sK1 = sK6
| ~ rpoint(sK1)
| ~ spl54_840
| ~ spl54_841 ),
inference(resolution,[],[f16346,f18235]) ).
fof(f18505,plain,
( sK1 = sK6
| ~ rpoint(sK1)
| ~ spl54_840
| ~ spl54_841
| spl54_932 ),
inference(forward_subsumption_resolution,[],[f18501,f18273]) ).
fof(f18507,plain,
( ~ rpoint(sK1)
| ~ spl54_840
| ~ spl54_841
| spl54_932 ),
inference(forward_subsumption_resolution,[],[f18505,f708]) ).
fof(f18509,plain,
( $false
| ~ spl54_840
| ~ spl54_841
| spl54_932 ),
inference(forward_subsumption_resolution,[],[f18507,f439]) ).
fof(f18510,plain,
( ~ spl54_840
| ~ spl54_841
| spl54_932 ),
inference(avatar_contradiction_clause,[],[f18509]) ).
fof(f19510,plain,
( rR(sK6,sK5,vd1371)
| rR(vd1371,sK6,sK5)
| rR(sK5,sK6,vd1371)
| vd1371 = sK5
| vd1371 = sK6
| sK5 = sK6
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| spl54_73
| ~ spl54_840 ),
inference(resolution,[],[f18116,f14565]) ).
fof(f19597,definition,
( spl54_986
<=> rR(sK5,sK6,vd1371) ),
introduced(definition,[new_symbols(definition,[spl54_986])],[avatar_definition]) ).
fof(f19598,plain,
( ~ rR(sK5,sK6,vd1371)
| spl54_986 ),
inference(avatar_component_clause,[],[f19597]) ).
fof(f19599,plain,
( rR(sK5,sK6,vd1371)
| ~ spl54_986 ),
inference(avatar_component_clause,[],[f19597]) ).
fof(f19601,definition,
( spl54_987
<=> rR(vd1371,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl54_987])],[avatar_definition]) ).
fof(f19602,plain,
( ~ rR(vd1371,sK6,sK5)
| spl54_987 ),
inference(avatar_component_clause,[],[f19601]) ).
fof(f19603,plain,
( rR(vd1371,sK6,sK5)
| ~ spl54_987 ),
inference(avatar_component_clause,[],[f19601]) ).
fof(f19625,plain,
( rR(sK5,sK6,sK1)
| ~ rpoint(sK5)
| ~ spl54_986 ),
inference(resolution,[],[f19599,f2395]) ).
fof(f19640,plain,
( ~ rpoint(sK5)
| spl54_839
| ~ spl54_986 ),
inference(forward_subsumption_resolution,[],[f19625,f14386]) ).
fof(f19647,plain,
( $false
| spl54_839
| ~ spl54_986 ),
inference(forward_subsumption_resolution,[],[f19640,f460]) ).
fof(f19648,plain,
( spl54_839
| ~ spl54_986 ),
inference(avatar_contradiction_clause,[],[f19647]) ).
fof(f19673,plain,
( ~ rR(vd1371,sK1,sK5)
| ~ rpoint(sK5)
| ~ spl54_987 ),
inference(resolution,[],[f19603,f6129]) ).
fof(f19951,plain,
( sK1 = sK6
| ~ rpoint(sK6)
| ~ rpoint(sK1)
| spl54_934 ),
inference(resolution,[],[f18281,f962]) ).
fof(f19952,plain,
( ~ rpoint(sK6)
| ~ rpoint(sK1)
| spl54_934 ),
inference(forward_subsumption_resolution,[],[f19951,f708]) ).
fof(f19953,plain,
( ~ rpoint(sK1)
| spl54_934 ),
inference(forward_subsumption_resolution,[],[f19952,f462]) ).
fof(f19954,plain,
( $false
| spl54_934 ),
inference(forward_subsumption_resolution,[],[f19953,f439]) ).
fof(f19955,plain,
spl54_934,
inference(avatar_contradiction_clause,[],[f19954]) ).
fof(f20076,plain,
( ~ rline(sK10(sK1,sK6))
| ~ ron(sK1,sK10(sK1,sK6))
| ron(vd1371,sK10(sK1,sK6))
| ~ spl54_840
| ~ spl54_848 ),
inference(resolution,[],[f14425,f18235]) ).
fof(f20084,plain,
( ~ ron(sK1,sK10(sK1,sK6))
| ron(vd1371,sK10(sK1,sK6))
| ~ spl54_840
| ~ spl54_848
| ~ spl54_934 ),
inference(forward_subsumption_resolution,[],[f20076,f18280]) ).
fof(f20089,plain,
( ron(vd1371,sK10(sK1,sK6))
| ~ spl54_840
| ~ spl54_848
| ~ spl54_932
| ~ spl54_934 ),
inference(forward_subsumption_resolution,[],[f20084,f18272]) ).
fof(f20205,plain,
( ~ rR(vd1371,sK1,sK5)
| ~ spl54_987 ),
inference(forward_subsumption_resolution,[],[f19673,f460]) ).
fof(f20259,plain,
( rR(sK6,sK5,vd1371)
| rR(sK5,sK6,vd1371)
| vd1371 = sK5
| vd1371 = sK6
| sK5 = sK6
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| spl54_73
| ~ spl54_840
| spl54_987 ),
inference(forward_subsumption_resolution,[],[f19510,f19602]) ).
fof(f20264,plain,
( ! [X0] :
( ~ rR(sK1,sK5,vd1371)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| sK1 = sK5
| ~ rline(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK1) )
| spl54_13
| spl54_15
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f18351,f1578]) ).
fof(f20279,plain,
( rR(sK6,sK5,vd1371)
| vd1371 = sK5
| vd1371 = sK6
| sK5 = sK6
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| spl54_73
| ~ spl54_840
| spl54_986
| spl54_987 ),
inference(forward_subsumption_resolution,[],[f20259,f19598]) ).
fof(f20284,plain,
( ! [X0] :
( ~ rR(sK1,sK5,vd1371)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK1) )
| spl54_13
| spl54_15
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f20264,f706]) ).
fof(f20296,plain,
( rR(sK6,sK5,vd1371)
| vd1371 = sK6
| sK5 = sK6
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| spl54_15
| spl54_73
| ~ spl54_840
| spl54_986
| spl54_987 ),
inference(forward_subsumption_resolution,[],[f20279,f1588]) ).
fof(f20301,plain,
( ! [X0] :
( ~ rR(sK1,sK5,vd1371)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK5)
| ~ rpoint(sK1) )
| spl54_13
| spl54_15
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f20284,f438]) ).
fof(f20311,plain,
( rR(sK6,sK5,vd1371)
| sK5 = sK6
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| spl54_15
| spl54_73
| ~ spl54_840
| spl54_986
| spl54_987 ),
inference(forward_subsumption_resolution,[],[f20296,f2175]) ).
fof(f20313,definition,
( spl54_997
<=> rR(sK6,sK5,vd1371) ),
introduced(definition,[new_symbols(definition,[spl54_997])],[avatar_definition]) ).
fof(f20315,plain,
( rR(sK6,sK5,vd1371)
| ~ spl54_997 ),
inference(avatar_component_clause,[],[f20313]) ).
fof(f20330,plain,
( ! [X0] :
( ~ rR(sK1,sK5,vd1371)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| ~ rpoint(sK1) )
| spl54_13
| spl54_15
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f20301,f460]) ).
fof(f20340,plain,
( rR(sK6,sK5,vd1371)
| ~ rpoint(vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| spl54_15
| spl54_73
| ~ spl54_840
| spl54_986
| spl54_987 ),
inference(forward_subsumption_resolution,[],[f20311,f707]) ).
fof(f20343,plain,
( ! [X0] :
( ~ rR(sK1,sK5,vd1371)
| ~ ron(sK5,X0)
| ~ ron(sK1,X0)
| ~ rline(X0) )
| spl54_13
| spl54_15
| ~ spl54_840 ),
inference(forward_subsumption_resolution,[],[f20330,f439]) ).
fof(f20349,plain,
( rR(sK6,sK5,vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK6)
| spl54_15
| spl54_73
| ~ spl54_840
| spl54_986
| spl54_987 ),
inference(forward_subsumption_resolution,[],[f20340,f438]) ).
fof(f20353,definition,
( spl54_1001
<=> rR(sK1,sK5,vd1371) ),
introduced(definition,[new_symbols(definition,[spl54_1001])],[avatar_definition]) ).
fof(f20355,plain,
( ~ rR(sK1,sK5,vd1371)
| spl54_1001 ),
inference(avatar_component_clause,[],[f20353]) ).
fof(f20356,plain,
( spl54_843
| ~ spl54_1001
| spl54_13
| spl54_15
| ~ spl54_840 ),
inference(avatar_split_clause,[],[f20343,f14388,f1587,f1577,f20353,f14401]) ).
fof(f20360,plain,
( rR(sK6,sK5,vd1371)
| ~ rpoint(sK6)
| spl54_15
| spl54_73
| ~ spl54_840
| spl54_986
| spl54_987 ),
inference(forward_subsumption_resolution,[],[f20349,f460]) ).
fof(f20366,plain,
( rR(sK6,sK5,vd1371)
| spl54_15
| spl54_73
| ~ spl54_840
| spl54_986
| spl54_987 ),
inference(forward_subsumption_resolution,[],[f20360,f462]) ).
fof(f20367,plain,
( spl54_997
| spl54_15
| spl54_73
| ~ spl54_840
| spl54_986
| spl54_987 ),
inference(avatar_split_clause,[],[f20366,f19601,f19597,f14388,f2174,f1587,f20313]) ).
fof(f20491,plain,
( vf(sK5,vd1371) = vplus(vf(sK5,sK6),vf(sK6,vd1371))
| ~ rpoint(vd1371)
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ spl54_997 ),
inference(resolution,[],[f20315,f950]) ).
fof(f20496,plain,
( vf(sK5,vd1371) = vplus(vf(sK5,sK6),vf(sK6,vd1371))
| ~ rpoint(sK6)
| ~ rpoint(sK5)
| ~ spl54_997 ),
inference(forward_subsumption_resolution,[],[f20491,f438]) ).
fof(f20500,plain,
( vf(sK5,vd1371) = vplus(vf(sK5,sK6),vf(sK6,vd1371))
| ~ rpoint(sK5)
| ~ spl54_997 ),
inference(forward_subsumption_resolution,[],[f20496,f462]) ).
fof(f20504,plain,
( vf(sK5,vd1371) = vplus(vf(sK5,sK6),vf(sK6,vd1371))
| ~ spl54_997 ),
inference(forward_subsumption_resolution,[],[f20500,f460]) ).
fof(f20506,plain,
( vf(sK5,vd1371) = vplus(vf(sK5,sK6),sK7(sK6,vd1371))
| ~ spl54_997 ),
inference(forward_demodulation,[],[f20504,f2847]) ).
fof(f20507,plain,
( vf(sK5,vd1371) = vplus(vf(sK6,sK5),sK7(sK6,vd1371))
| ~ spl54_997 ),
inference(forward_demodulation,[],[f20506,f1941]) ).
fof(f20508,plain,
( vf(sK5,vd1371) = vplus(sK7(sK6,sK5),sK7(sK6,vd1371))
| ~ spl54_997 ),
inference(forward_demodulation,[],[f20507,f2850]) ).
fof(f20509,plain,
( sF53 = vf(sK5,vd1371)
| ~ spl54_997 ),
inference(forward_demodulation,[],[f20508,f2893]) ).
fof(f20510,plain,
( sF52 = sF53
| ~ spl54_997 ),
inference(forward_demodulation,[],[f20509,f1833]) ).
fof(f20511,plain,
( $false
| ~ spl54_997 ),
inference(forward_subsumption_resolution,[],[f20510,f1502]) ).
fof(f20512,plain,
~ spl54_997,
inference(avatar_contradiction_clause,[],[f20511]) ).
fof(f20864,plain,
( rR(sK1,vd1371,sK5)
| rR(sK5,sK1,vd1371)
| rR(vd1371,sK1,sK5)
| vd1371 = sK5
| vd1371 = sK1
| ~ rpoint(vd1371)
| ~ spl54_840
| ~ spl54_848
| ~ spl54_932
| ~ spl54_934 ),
inference(resolution,[],[f18328,f20089]) ).
fof(f20873,plain,
( rR(sK5,sK1,vd1371)
| rR(vd1371,sK1,sK5)
| vd1371 = sK5
| vd1371 = sK1
| ~ rpoint(vd1371)
| ~ spl54_840
| ~ spl54_848
| spl54_918
| ~ spl54_932
| ~ spl54_934 ),
inference(forward_subsumption_resolution,[],[f20864,f16590]) ).
fof(f20874,plain,
( rR(sK5,sK1,vd1371)
| vd1371 = sK5
| vd1371 = sK1
| ~ rpoint(vd1371)
| ~ spl54_840
| ~ spl54_848
| spl54_918
| ~ spl54_932
| ~ spl54_934
| ~ spl54_987 ),
inference(forward_subsumption_resolution,[],[f20873,f20205]) ).
fof(f20875,plain,
( rR(sK5,sK1,vd1371)
| vd1371 = sK1
| ~ rpoint(vd1371)
| spl54_15
| ~ spl54_840
| ~ spl54_848
| spl54_918
| ~ spl54_932
| ~ spl54_934
| ~ spl54_987 ),
inference(forward_subsumption_resolution,[],[f20874,f1588]) ).
fof(f20876,plain,
( rR(sK5,sK1,vd1371)
| ~ rpoint(vd1371)
| spl54_13
| spl54_15
| ~ spl54_840
| ~ spl54_848
| spl54_918
| ~ spl54_932
| ~ spl54_934
| ~ spl54_987 ),
inference(forward_subsumption_resolution,[],[f20875,f1578]) ).
fof(f20877,plain,
( rR(sK5,sK1,vd1371)
| spl54_13
| spl54_15
| ~ spl54_840
| ~ spl54_848
| spl54_918
| ~ spl54_932
| ~ spl54_934
| ~ spl54_987 ),
inference(forward_subsumption_resolution,[],[f20876,f438]) ).
fof(f20878,plain,
( rR(sK5,sK1,sK6)
| ~ rpoint(sK5)
| spl54_13
| spl54_15
| ~ spl54_840
| ~ spl54_848
| spl54_918
| ~ spl54_932
| ~ spl54_934
| ~ spl54_987 ),
inference(resolution,[],[f20877,f2396]) ).
fof(f20893,plain,
( ~ rpoint(sK5)
| spl54_13
| spl54_15
| ~ spl54_840
| spl54_844
| ~ spl54_848
| spl54_918
| ~ spl54_932
| ~ spl54_934
| ~ spl54_987 ),
inference(forward_subsumption_resolution,[],[f20878,f14406]) ).
fof(f20899,plain,
( $false
| spl54_13
| spl54_15
| ~ spl54_840
| spl54_844
| ~ spl54_848
| spl54_918
| ~ spl54_932
| ~ spl54_934
| ~ spl54_987 ),
inference(forward_subsumption_resolution,[],[f20893,f460]) ).
fof(f20900,plain,
( spl54_13
| spl54_15
| ~ spl54_840
| spl54_844
| ~ spl54_848
| spl54_918
| ~ spl54_932
| ~ spl54_934
| ~ spl54_987 ),
inference(avatar_contradiction_clause,[],[f20899]) ).
fof(f20914,plain,
( rR(sK1,sK5,vd1371)
| ~ rpoint(sK5)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ spl54_918 ),
inference(resolution,[],[f16589,f898]) ).
fof(f20922,plain,
( ~ rpoint(sK5)
| ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ spl54_918
| spl54_1001 ),
inference(forward_subsumption_resolution,[],[f20914,f20355]) ).
fof(f20927,plain,
( ~ rpoint(sK1)
| ~ rpoint(vd1371)
| ~ spl54_918
| spl54_1001 ),
inference(forward_subsumption_resolution,[],[f20922,f460]) ).
fof(f20932,plain,
( ~ rpoint(vd1371)
| ~ spl54_918
| spl54_1001 ),
inference(forward_subsumption_resolution,[],[f20927,f439]) ).
fof(f20935,plain,
( $false
| ~ spl54_918
| spl54_1001 ),
inference(forward_subsumption_resolution,[],[f20932,f438]) ).
fof(f20936,plain,
( ~ spl54_918
| spl54_1001 ),
inference(avatar_contradiction_clause,[],[f20935]) ).
cnf(s141,plain,
~ spl54_73,
inference(sat_conversion,[],[f3148]) ).
cnf(s602,plain,
( spl54_587
| spl54_588 ),
inference(sat_conversion,[],[f10236]) ).
cnf(s604,plain,
( spl54_590
| spl54_591 ),
inference(sat_conversion,[],[f10264]) ).
cnf(s660,plain,
( spl54_588
| spl54_656 ),
inference(sat_conversion,[],[f11007]) ).
cnf(s661,plain,
( spl54_591
| spl54_657 ),
inference(sat_conversion,[],[f11026]) ).
cnf(s667,plain,
~ spl54_588,
inference(sat_conversion,[],[f11203]) ).
cnf(s670,plain,
( spl54_13
| spl54_15
| ~ spl54_591 ),
inference(sat_conversion,[],[f11339]) ).
cnf(s673,plain,
( spl54_588
| spl54_671 ),
inference(sat_conversion,[],[f11760]) ).
cnf(s852,plain,
( spl54_838
| ~ spl54_839
| ~ spl54_840 ),
inference(sat_conversion,[],[f14391]) ).
cnf(s853,plain,
( ~ spl54_840
| spl54_841 ),
inference(sat_conversion,[],[f14395]) ).
cnf(s860,plain,
( spl54_13
| spl54_15
| ~ spl54_840
| spl54_848 ),
inference(sat_conversion,[],[f14426]) ).
cnf(s868,plain,
( spl54_588
| spl54_803 ),
inference(sat_conversion,[],[f14532]) ).
cnf(s869,plain,
( spl54_591
| spl54_808 ),
inference(sat_conversion,[],[f14533]) ).
cnf(s893,plain,
( ~ spl54_590
| ~ spl54_657
| ~ spl54_808
| ~ spl54_873 ),
inference(sat_conversion,[],[f15450]) ).
cnf(s930,plain,
( spl54_839
| spl54_840 ),
inference(sat_conversion,[],[f16429]) ).
cnf(s935,plain,
( spl54_839
| ~ spl54_844 ),
inference(sat_conversion,[],[f16584]) ).
cnf(s937,plain,
( ~ spl54_840
| ~ spl54_843
| spl54_873 ),
inference(sat_conversion,[],[f16658]) ).
cnf(s943,plain,
( spl54_840
| spl54_911 ),
inference(sat_conversion,[],[f16852]) ).
cnf(s945,plain,
( ~ spl54_844
| ~ spl54_911 ),
inference(sat_conversion,[],[f16857]) ).
cnf(s946,plain,
( ~ spl54_839
| spl54_844 ),
inference(sat_conversion,[],[f16871]) ).
cnf(s956,plain,
~ spl54_13,
inference(sat_conversion,[],[f17057]) ).
cnf(s976,plain,
( ~ spl54_587
| ~ spl54_656
| ~ spl54_671
| ~ spl54_803
| ~ spl54_838 ),
inference(sat_conversion,[],[f17756]) ).
cnf(s978,plain,
( ~ spl54_15
| spl54_839 ),
inference(sat_conversion,[],[f17760]) ).
cnf(s994,plain,
( ~ spl54_840
| ~ spl54_841
| spl54_932 ),
inference(sat_conversion,[],[f18510]) ).
cnf(s1037,plain,
( spl54_839
| ~ spl54_986 ),
inference(sat_conversion,[],[f19648]) ).
cnf(s1046,plain,
spl54_934,
inference(sat_conversion,[],[f19955]) ).
cnf(s1056,plain,
( spl54_13
| spl54_15
| ~ spl54_840
| spl54_843
| ~ spl54_1001 ),
inference(sat_conversion,[],[f20356]) ).
cnf(s1059,plain,
( spl54_15
| spl54_73
| ~ spl54_840
| spl54_986
| spl54_987
| spl54_997 ),
inference(sat_conversion,[],[f20367]) ).
cnf(s1064,plain,
~ spl54_997,
inference(sat_conversion,[],[f20512]) ).
cnf(s1073,plain,
( spl54_13
| spl54_15
| ~ spl54_840
| spl54_844
| ~ spl54_848
| spl54_918
| ~ spl54_932
| ~ spl54_934
| ~ spl54_987 ),
inference(sat_conversion,[],[f20900]) ).
cnf(s1074,plain,
( ~ spl54_918
| spl54_1001 ),
inference(sat_conversion,[],[f20936]) ).
cnf(s1075,plain,
( spl54_15
| spl54_73
| ~ spl54_840
| spl54_986
| spl54_987 ),
inference(rat,[],[s1059,s1064]) ).
cnf(s1114,plain,
( spl54_15
| ~ spl54_840
| spl54_848 ),
inference(rat,[],[s860,s956]) ).
cnf(s1159,plain,
( spl54_15
| ~ spl54_591 ),
inference(rat,[],[s670,s956]) ).
cnf(s1162,plain,
spl54_803,
inference(rat,[],[s868,s667]) ).
cnf(s1164,plain,
spl54_671,
inference(rat,[],[s673,s667]) ).
cnf(s1171,plain,
spl54_656,
inference(rat,[],[s660,s667]) ).
cnf(s1186,plain,
spl54_587,
inference(rat,[],[s602,s667]) ).
cnf(s1187,plain,
~ spl54_838,
inference(rat,[],[s976,s1171,s1162,s1164,s1186]) ).
cnf(s1417,plain,
( spl54_839
| spl54_15 ),
inference(rat,[],[s1073,s1074,s994,s1056,s1075,s853,s1114,s937,s930,s935,s1037,s893,s604,s869,s661,s1159,s956,s1046,s141]) ).
cnf(s1418,plain,
~ spl54_839,
inference(rat,[],[s943,s945,s852,s946,s1187]) ).
cnf(s1420,plain,
~ spl54_15,
inference(rat,[],[s978,s1418]) ).
cnf(s1423,plain,
$false,
inference(rat,[],[s1417,s1420,s1418]) ).
fof(f20941,plain,
$false,
inference(avatar_sat_refutation,[],[s1423]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO334+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.11/0.39 % Computer : n008.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 08:07:10 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.86/2.46 % (908235)Detected formulas, will run a generic FOF schedule.
% 10.86/2.46 % (908246)dis-21_1_sil=8000:lcm=predicate:random_seed=2836398920: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)
% 10.86/2.46 % (908246)Instruction limit reached!
% 10.86/2.46 % (908246)------------------------------
% 10.86/2.46 % (908246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.86/2.46 % (908246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.86/2.46 % (908246)CaDiCaL version: 2.1.3
% 10.86/2.46 % (908246)Termination reason: Instruction limit
% 10.86/2.46 % (908246)Termination phase: Saturation
% 10.86/2.46 % (908246)Time elapsed: 0.031 s
% 10.86/2.46 % (908246)Peak memory usage: 89 MB
% 10.86/2.46 % (908246)Instructions burned: 133 (million)
% 10.86/2.46 % (908240)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=3633095463:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.86/2.46 % (908242)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=3244349412:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.86/2.46 % (908243)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=335607511:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.86/2.46 % (908241)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=1212865555:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.86/2.46 % (908243)Refutation not found, incomplete strategy
% 10.86/2.46 % (908243)------------------------------
% 10.86/2.46 % (908243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.86/2.46 % (908243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.86/2.46 % (908243)CaDiCaL version: 2.1.3
% 10.86/2.46 % (908243)Termination reason: Refutation not found, incomplete strategy
% 10.86/2.46 % (908243)Time elapsed: 0.002 s
% 10.86/2.46 % (908243)Peak memory usage: 88 MB
% 10.86/2.46 % (908243)Instructions burned: 1 (million)
% 10.86/2.46 % (908244)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2036825572:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.86/2.46 % (908245)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=841132614:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.86/2.46 % (908244)Instruction limit reached!
% 10.86/2.46 % (908244)------------------------------
% 10.86/2.46 % (908244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.86/2.46 % (908244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.86/2.46 % (908244)CaDiCaL version: 2.1.3
% 10.86/2.46 % (908244)Termination reason: Instruction limit
% 10.86/2.46 % (908244)Termination phase: Saturation
% 10.86/2.46 % (908244)Time elapsed: 0.061 s
% 10.86/2.46 % (908244)Peak memory usage: 89 MB
% 10.86/2.46 % (908244)Instructions burned: 122 (million)
% 10.86/2.46 % (908249)lrs+10_1_sil=8000:sp=occurrence:random_seed=2216880052:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.86/2.46 % (908245)Instruction limit reached!
% 10.86/2.46 % (908245)------------------------------
% 10.86/2.46 % (908245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.86/2.46 % (908245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.86/2.46 % (908245)CaDiCaL version: 2.1.3
% 10.86/2.46 % (908245)Termination reason: Instruction limit
% 10.86/2.46 % (908245)Termination phase: Saturation
% 10.86/2.46 % (908245)Time elapsed: 0.081 s
% 10.86/2.46 % (908245)Peak memory usage: 90 MB
% 10.86/2.46 % (908245)Instructions burned: 140 (million)
% 10.86/2.46 % (908249)Instruction limit reached!
% 10.86/2.46 % (908249)------------------------------
% 10.86/2.46 % (908249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.86/2.46 % (908249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.86/2.46 % (908249)CaDiCaL version: 2.1.3
% 10.86/2.46 % (908249)Termination reason: Instruction limit
% 10.86/2.46 % (908249)Termination phase: Saturation
% 10.86/2.46 % (908249)Time elapsed: 0.082 s
% 10.86/2.46 % (908249)Peak memory usage: 92 MB
% 10.86/2.46 % (908249)Instructions burned: 285 (million)
% 10.86/2.46 % (908255)lrs+10_1_sil=32000:urr=on:br=off:random_seed=448147371:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 16.77/3.30 % (908255)Refutation not found, incomplete strategy
% 16.77/3.30 % (908255)------------------------------
% 16.77/3.30 % (908255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.77/3.30 % (908255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.77/3.30 % (908255)CaDiCaL version: 2.1.3
% 16.77/3.30 % (908255)Termination reason: Refutation not found, incomplete strategy
% 16.77/3.30 % (908255)Time elapsed: 0.004 s
% 16.77/3.30 % (908255)Peak memory usage: 89 MB
% 16.77/3.30 % (908255)Instructions burned: 4 (million)
% 16.77/3.30 % (908257)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1289598019:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 16.77/3.30 % (908243)------------------------------
% 16.77/3.30 % (908243)------------------------------
% 16.77/3.30 % (908258)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=2963422957:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 16.77/3.30 % (908258)Instruction limit reached!
% 16.77/3.30 % (908258)------------------------------
% 16.77/3.30 % (908258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.77/3.30 % (908258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.77/3.30 % (908258)CaDiCaL version: 2.1.3
% 16.77/3.30 % (908258)Termination reason: Instruction limit
% 16.77/3.30 % (908258)Termination phase: Saturation
% 16.77/3.30 % (908258)Time elapsed: 0.064 s
% 16.77/3.30 % (908258)Peak memory usage: 92 MB
% 16.77/3.30 % (908258)Instructions burned: 251 (million)
% 16.77/3.30 % (908262)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3018610355:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 16.77/3.30 % (908263)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1948833311:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 16.77/3.30 % (908257)Instruction limit reached!
% 16.77/3.30 % (908257)------------------------------
% 16.77/3.30 % (908257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.77/3.30 % (908257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.77/3.30 % (908257)CaDiCaL version: 2.1.3
% 16.77/3.30 % (908257)Termination reason: Instruction limit
% 16.77/3.30 % (908257)Termination phase: Saturation
% 16.77/3.30 % (908257)Time elapsed: 0.175 s
% 16.77/3.30 % (908257)Peak memory usage: 91 MB
% 16.77/3.30 % (908257)Instructions burned: 326 (million)
% 16.77/3.30 % (908255)------------------------------
% 16.77/3.30 % (908255)------------------------------
% 16.77/3.30 % (908266)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=568970929:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 16.77/3.30 % (908262)Instruction limit reached!
% 16.77/3.30 % (908262)------------------------------
% 16.77/3.30 % (908262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.77/3.30 % (908262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.77/3.30 % (908262)CaDiCaL version: 2.1.3
% 16.77/3.30 % (908262)Termination reason: Instruction limit
% 16.77/3.30 % (908262)Termination phase: Saturation
% 16.77/3.30 % (908262)Time elapsed: 0.150 s
% 16.77/3.30 % (908262)Peak memory usage: 89 MB
% 16.77/3.30 % (908262)Instructions burned: 295 (million)
% 16.77/3.30 % (908267)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4088277420:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 16.77/3.30 % (908266)Instruction limit reached!
% 16.77/3.30 % (908266)------------------------------
% 16.77/3.30 % (908266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.77/3.30 % (908266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.77/3.30 % (908266)CaDiCaL version: 2.1.3
% 16.77/3.30 % (908266)Termination reason: Instruction limit
% 16.77/3.30 % (908266)Termination phase: Saturation
% 16.77/3.30 % (908266)Time elapsed: 0.058 s
% 16.77/3.30 % (908266)Peak memory usage: 90 MB
% 16.77/3.30 % (908266)Instructions burned: 113 (million)
% 16.77/3.30 % (908267)Refutation not found, incomplete strategy
% 16.77/3.30 % (908267)------------------------------
% 16.77/3.30 % (908267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.77/3.30 % (908267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.77/3.30 % (908267)CaDiCaL version: 2.1.3
% 16.77/3.30 % (908267)Termination reason: Refutation not found, incomplete strategy
% 19.45/3.70 % (908267)Time elapsed: 0.025 s
% 19.45/3.70 % (908267)Peak memory usage: 89 MB
% 19.45/3.70 % (908267)Instructions burned: 52 (million)
% 19.45/3.70 % (908269)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3603558088:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 19.45/3.70 % (908271)lrs+10_1_sil=8000:sp=occurrence:random_seed=812631805:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 19.45/3.70 % (908269)Instruction limit reached!
% 19.45/3.70 % (908269)------------------------------
% 19.45/3.70 % (908269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.45/3.70 % (908269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.45/3.70 % (908269)CaDiCaL version: 2.1.3
% 19.45/3.70 % (908269)Termination reason: Instruction limit
% 19.45/3.70 % (908269)Termination phase: Saturation
% 19.45/3.70 % (908269)Time elapsed: 0.057 s
% 19.45/3.70 % (908269)Peak memory usage: 89 MB
% 19.45/3.70 % (908269)Instructions burned: 115 (million)
% 19.45/3.70 % (908274)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2320098916:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 19.45/3.70 % (908274)Refutation not found, incomplete strategy
% 19.45/3.70 % (908274)------------------------------
% 19.45/3.70 % (908274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.45/3.70 % (908274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.45/3.70 % (908274)CaDiCaL version: 2.1.3
% 19.45/3.70 % (908274)Termination reason: Refutation not found, incomplete strategy
% 19.45/3.70 % (908274)Time elapsed: 0.009 s
% 19.45/3.70 % (908274)Peak memory usage: 90 MB
% 19.45/3.70 % (908274)Instructions burned: 31 (million)
% 19.45/3.70 % (908267)------------------------------
% 19.45/3.70 % (908267)------------------------------
% 19.45/3.70 % (908274)------------------------------
% 19.45/3.70 % (908274)------------------------------
% 19.45/3.70 % (908276)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=951783259:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 19.45/3.70 % (908278)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=266791839:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 19.45/3.70 % (908278)Instruction limit reached!
% 19.45/3.70 % (908278)------------------------------
% 19.45/3.70 % (908278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.45/3.70 % (908278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.45/3.70 % (908278)CaDiCaL version: 2.1.3
% 19.45/3.70 % (908278)Termination reason: Instruction limit
% 19.45/3.70 % (908278)Termination phase: Saturation
% 19.45/3.70 % (908278)Time elapsed: 0.062 s
% 19.45/3.70 % (908278)Peak memory usage: 92 MB
% 19.45/3.70 % (908278)Instructions burned: 136 (million)
% 19.45/3.70 % (908271)Instruction limit reached!
% 19.45/3.70 % (908271)------------------------------
% 19.45/3.70 % (908271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.45/3.70 % (908271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.45/3.70 % (908271)CaDiCaL version: 2.1.3
% 19.45/3.70 % (908271)Termination reason: Instruction limit
% 19.45/3.70 % (908271)Termination phase: Saturation
% 20.48/3.70 % (908271)Time elapsed: 0.493 s
% 20.48/3.70 % (908271)Peak memory usage: 98 MB
% 20.48/3.70 % (908271)Instructions burned: 907 (million)
% 20.48/3.70 % (908280)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3266773279:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 20.48/3.70 % (908281)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4262901762:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 20.48/3.70 % (908263)Instruction limit reached!
% 20.48/3.70 % (908263)------------------------------
% 20.48/3.70 % (908263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.48/3.70 % (908263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.70 % (908263)CaDiCaL version: 2.1.3
% 20.48/3.70 % (908263)Termination reason: Instruction limit
% 20.48/3.70 % (908263)Termination phase: Saturation
% 20.48/3.70 % (908263)Time elapsed: 0.954 s
% 20.48/3.70 % (908263)Peak memory usage: 142 MB
% 20.48/3.70 % (908263)Instructions burned: 2352 (million)
% 20.48/3.70 % (908284)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=3056266988:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 20.48/3.70 % (908284)Instruction limit reached!
% 20.48/3.70 % (908284)------------------------------
% 20.48/3.70 % (908284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.48/3.70 % (908284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.70 % (908284)CaDiCaL version: 2.1.3
% 20.48/3.70 % (908284)Termination reason: Instruction limit
% 20.48/3.70 % (908284)Termination phase: Saturation
% 20.48/3.70 % (908284)Time elapsed: 0.032 s
% 20.48/3.70 % (908284)Peak memory usage: 92 MB
% 20.48/3.70 % (908284)Instructions burned: 127 (million)
% 20.48/3.70 % (908286)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3612595390:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 20.48/3.70 % (908286)Instruction limit reached!
% 20.48/3.70 % (908286)------------------------------
% 20.48/3.70 % (908286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.48/3.70 % (908286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.70 % (908286)CaDiCaL version: 2.1.3
% 20.48/3.70 % (908286)Termination reason: Instruction limit
% 20.48/3.70 % (908286)Termination phase: Saturation
% 20.48/3.70 % (908286)Time elapsed: 0.041 s
% 20.48/3.70 % (908286)Peak memory usage: 91 MB
% 20.48/3.70 % (908286)Instructions burned: 134 (million)
% 20.48/3.70 % (908280)Instruction limit reached!
% 20.48/3.70 % (908280)------------------------------
% 20.48/3.70 % (908280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.48/3.70 % (908280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.70 % (908280)CaDiCaL version: 2.1.3
% 20.48/3.70 % (908280)Termination reason: Instruction limit
% 20.48/3.70 % (908280)Termination phase: Saturation
% 20.48/3.70 % (908280)Time elapsed: 0.371 s
% 20.48/3.70 % (908280)Peak memory usage: 97 MB
% 20.48/3.70 % (908280)Instructions burned: 593 (million)
% 20.48/3.70 % (908288)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=175030023:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 20.48/3.70 % (908288)Refutation not found, incomplete strategy
% 20.48/3.70 % (908288)------------------------------
% 20.48/3.70 % (908288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.48/3.70 % (908288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.70 % (908288)CaDiCaL version: 2.1.3
% 20.48/3.70 % (908288)Termination reason: Refutation not found, incomplete strategy
% 20.48/3.70 % (908288)Time elapsed: 0.001 s
% 20.48/3.70 % (908288)Peak memory usage: 88 MB
% 20.48/3.70 % (908288)Instructions burned: 1 (million)
% 20.48/3.70 % (908289)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1483784003:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 20.48/3.70 % (908289)Refutation not found, incomplete strategy
% 20.48/3.70 % (908289)------------------------------
% 20.48/3.70 % (908289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.48/3.70 % (908289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.70 % (908289)CaDiCaL version: 2.1.3
% 20.48/3.70 % (908289)Termination reason: Refutation not found, incomplete strategy
% 20.48/3.70 % (908289)Time elapsed: 0.006 s
% 20.48/3.70 % (908289)Peak memory usage: 88 MB
% 20.48/3.70 % (908289)Instructions burned: 9 (million)
% 20.48/3.70 % (908288)------------------------------
% 20.48/3.70 % (908288)------------------------------
% 20.48/3.70 % (908292)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=3950310661:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi)
% 20.48/3.70 % (908289)------------------------------
% 20.48/3.70 % (908289)------------------------------
% 20.48/3.70 % (908294)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=804960051:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2977 on theBenchmark for (2977ds/150Mi)
% 20.48/3.70 % (908294)Instruction limit reached!
% 20.48/3.70 % (908294)------------------------------
% 20.48/3.70 % (908294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.48/3.70 % (908294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.70 % (908294)CaDiCaL version: 2.1.3
% 20.48/3.70 % (908294)Termination reason: Instruction limit
% 20.48/3.70 % (908294)Termination phase: Saturation
% 20.48/3.70 % (908294)Time elapsed: 0.076 s
% 20.48/3.70 % (908294)Peak memory usage: 92 MB
% 20.48/3.70 % (908294)Instructions burned: 151 (million)
% 20.48/3.70 % (908240)First to succeed.
% 20.48/3.70 % (908296)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3177286919:i=14155:bd=all_2975 on theBenchmark for (2975ds/14155Mi)
% 20.48/3.70 % (908240)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-908235"
% 20.48/3.70 % (908240)Refutation found. Thanks to Tanya!
% 20.48/3.70 % SZS status Theorem for theBenchmark
% 20.48/3.70 % SZS output start Proof for theBenchmark
% See solution above
% 20.57/3.89 % (908240)------------------------------
% 20.57/3.89 % (908240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/3.89 % (908240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.89 % (908240)CaDiCaL version: 2.1.3
% 20.57/3.89 % (908240)Termination reason: Refutation
% 20.57/3.89 % (908240)Time elapsed: 2.432 s
% 20.57/3.89 % (908240)Peak memory usage: 151 MB
% 20.57/3.89 % (908240)Instructions burned: 4029 (million)
% 20.57/3.89 % (908240)------------------------------
% 20.57/3.89 % (908240)------------------------------
% 20.57/3.89 % (908235)Success in time 2.838 s
% 20.57/3.89 % Vampire exiting
%------------------------------------------------------------------------------