%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO167+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:51:44 AM UTC 2026
% Result : Theorem 10.31s 2.71s
% Output : Refutation 13.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 154
% Syntax : Number of formulae : 1285 ( 93 unt; 131 def)
% Number of atoms : 3460 ( 0 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 3931 (1756 ~;2000 |; 26 &)
% ( 131 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 33 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 137 ( 136 usr; 133 prp; 0-4 aty)
% Number of functors : 19 ( 19 usr; 17 con; 0-3 aty)
% Number of variables : 498 ( 0 sgn 492 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( colinear(a,b,c,l)
& colinear(d,e,f,m) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption1) ).
fof(f2,axiom,
( colinear(b,f,g,n)
& colinear(c,e,g,o) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption2) ).
fof(f3,axiom,
( colinear(b,d,h,p)
& colinear(a,e,h,q) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption3) ).
fof(f4,axiom,
( colinear(c,d,i,r)
& colinear(a,f,i,s) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption4) ).
fof(f5,axiom,
( line_equal(n,o)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal1) ).
fof(f6,axiom,
( line_equal(p,q)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal2) ).
fof(f7,axiom,
( line_equal(s,r)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal3) ).
fof(f8,axiom,
! [X0] :
( ( line_equal(X0,X0)
& incident(g,X0)
& incident(h,X0)
& incident(i,X0) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal4) ).
fof(f9,axiom,
! [X0,X1,X2,X3] :
( colinear(X0,X1,X2,X3)
=> incident(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',colinearity_elimination1) ).
fof(f10,axiom,
! [X0,X1,X2,X3] :
( colinear(X0,X1,X2,X3)
=> incident(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',colinearity_elimination2) ).
fof(f11,axiom,
! [X0,X1,X2,X3] :
( colinear(X0,X1,X2,X3)
=> incident(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',colinearity_elimination3) ).
fof(f12,axiom,
! [X0,X1] :
( incident(X0,X1)
=> point_equal(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_of_point_equal) ).
fof(f13,axiom,
! [X0,X1] :
( point_equal(X0,X1)
=> point_equal(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_point_equal) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( point_equal(X0,X1)
& point_equal(X1,X2) )
=> point_equal(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_point_equal) ).
fof(f15,axiom,
! [X0,X1] :
( incident(X0,X1)
=> line_equal(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_of_line_equal) ).
fof(f16,axiom,
! [X0,X1] :
( line_equal(X0,X1)
=> line_equal(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_line_equal) ).
fof(f17,axiom,
! [X0,X1,X2] :
( ( line_equal(X0,X1)
& line_equal(X1,X2) )
=> line_equal(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_line_equal) ).
fof(f18,axiom,
! [X0,X1,X2] :
( ( point_equal(X0,X1)
& incident(X1,X2) )
=> incident(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pcon) ).
fof(f19,axiom,
! [X0,X1,X2] :
( ( incident(X0,X1)
& line_equal(X1,X2) )
=> incident(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lcon) ).
fof(f20,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
( ( colinear(X0,X1,X2,X9)
& colinear(X3,X4,X5,X10)
& colinear(X1,X5,X6,X11)
& colinear(X2,X4,X6,X12)
& colinear(X1,X3,X7,X13)
& colinear(X0,X4,X7,X14)
& colinear(X2,X3,X8,X15)
& colinear(X0,X5,X8,X16) )
=> ( ? [X17] : colinear(X6,X7,X8,X17)
| incident(X0,X10)
| incident(X1,X10)
| incident(X2,X10)
| incident(X3,X9)
| incident(X4,X9)
| incident(X5,X9) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pappus1) ).
fof(f21,axiom,
! [X0,X1,X2,X3] :
( ( incident(X2,X0)
& incident(X2,X1)
& incident(X3,X0)
& incident(X3,X1) )
=> ( point_equal(X2,X3)
| line_equal(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique) ).
fof(f22,axiom,
! [X0,X1] :
( ( point_equal(X0,X0)
& point_equal(X1,X1) )
=> ? [X2] :
( incident(X0,X2)
& incident(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',line) ).
fof(f24,conjecture,
goal,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_to_be_proved) ).
fof(f25,negated_conjecture,
~ goal,
inference(negated_conjecture,[status(cth)],[f24]) ).
fof(f27,plain,
~ goal,
inference(flattening,[],[f25]) ).
fof(f28,plain,
( goal
| ~ line_equal(n,o) ),
inference(ennf_transformation,[],[f5]) ).
fof(f29,plain,
( goal
| ~ line_equal(p,q) ),
inference(ennf_transformation,[],[f6]) ).
fof(f30,plain,
( goal
| ~ line_equal(s,r) ),
inference(ennf_transformation,[],[f7]) ).
fof(f31,plain,
! [X0] :
( goal
| ~ line_equal(X0,X0)
| ~ incident(g,X0)
| ~ incident(h,X0)
| ~ incident(i,X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f32,plain,
! [X0] :
( goal
| ~ line_equal(X0,X0)
| ~ incident(g,X0)
| ~ incident(h,X0)
| ~ incident(i,X0) ),
inference(flattening,[],[f31]) ).
fof(f33,plain,
! [X0,X1,X2,X3] :
( incident(X0,X3)
| ~ colinear(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f9]) ).
fof(f34,plain,
! [X0,X1,X2,X3] :
( incident(X1,X3)
| ~ colinear(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f10]) ).
fof(f35,plain,
! [X0,X1,X2,X3] :
( incident(X2,X3)
| ~ colinear(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f11]) ).
fof(f36,plain,
! [X0,X1] :
( point_equal(X0,X0)
| ~ incident(X0,X1) ),
inference(ennf_transformation,[],[f12]) ).
fof(f37,plain,
! [X0,X1] :
( point_equal(X1,X0)
| ~ point_equal(X0,X1) ),
inference(ennf_transformation,[],[f13]) ).
fof(f38,plain,
! [X0,X1,X2] :
( point_equal(X0,X2)
| ~ point_equal(X0,X1)
| ~ point_equal(X1,X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f39,plain,
! [X0,X1,X2] :
( point_equal(X0,X2)
| ~ point_equal(X0,X1)
| ~ point_equal(X1,X2) ),
inference(flattening,[],[f38]) ).
fof(f40,plain,
! [X0,X1] :
( line_equal(X1,X1)
| ~ incident(X0,X1) ),
inference(ennf_transformation,[],[f15]) ).
fof(f41,plain,
! [X0,X1] :
( line_equal(X1,X0)
| ~ line_equal(X0,X1) ),
inference(ennf_transformation,[],[f16]) ).
fof(f42,plain,
! [X0,X1,X2] :
( line_equal(X0,X2)
| ~ line_equal(X0,X1)
| ~ line_equal(X1,X2) ),
inference(ennf_transformation,[],[f17]) ).
fof(f43,plain,
! [X0,X1,X2] :
( line_equal(X0,X2)
| ~ line_equal(X0,X1)
| ~ line_equal(X1,X2) ),
inference(flattening,[],[f42]) ).
fof(f44,plain,
! [X0,X1,X2] :
( incident(X0,X2)
| ~ point_equal(X0,X1)
| ~ incident(X1,X2) ),
inference(ennf_transformation,[],[f18]) ).
fof(f45,plain,
! [X0,X1,X2] :
( incident(X0,X2)
| ~ point_equal(X0,X1)
| ~ incident(X1,X2) ),
inference(flattening,[],[f44]) ).
fof(f46,plain,
! [X0,X1,X2] :
( incident(X0,X2)
| ~ incident(X0,X1)
| ~ line_equal(X1,X2) ),
inference(ennf_transformation,[],[f19]) ).
fof(f47,plain,
! [X0,X1,X2] :
( incident(X0,X2)
| ~ incident(X0,X1)
| ~ line_equal(X1,X2) ),
inference(flattening,[],[f46]) ).
fof(f48,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
( ? [X17] : colinear(X6,X7,X8,X17)
| incident(X0,X10)
| incident(X1,X10)
| incident(X2,X10)
| incident(X3,X9)
| incident(X4,X9)
| incident(X5,X9)
| ~ colinear(X0,X1,X2,X9)
| ~ colinear(X3,X4,X5,X10)
| ~ colinear(X1,X5,X6,X11)
| ~ colinear(X2,X4,X6,X12)
| ~ colinear(X1,X3,X7,X13)
| ~ colinear(X0,X4,X7,X14)
| ~ colinear(X2,X3,X8,X15)
| ~ colinear(X0,X5,X8,X16) ),
inference(ennf_transformation,[],[f20]) ).
fof(f49,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
( ? [X17] : colinear(X6,X7,X8,X17)
| incident(X0,X10)
| incident(X1,X10)
| incident(X2,X10)
| incident(X3,X9)
| incident(X4,X9)
| incident(X5,X9)
| ~ colinear(X0,X1,X2,X9)
| ~ colinear(X3,X4,X5,X10)
| ~ colinear(X1,X5,X6,X11)
| ~ colinear(X2,X4,X6,X12)
| ~ colinear(X1,X3,X7,X13)
| ~ colinear(X0,X4,X7,X14)
| ~ colinear(X2,X3,X8,X15)
| ~ colinear(X0,X5,X8,X16) ),
inference(flattening,[],[f48]) ).
fof(f50,plain,
! [X0,X1,X2,X3] :
( point_equal(X2,X3)
| line_equal(X0,X1)
| ~ incident(X2,X0)
| ~ incident(X2,X1)
| ~ incident(X3,X0)
| ~ incident(X3,X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f51,plain,
! [X0,X1,X2,X3] :
( point_equal(X2,X3)
| line_equal(X0,X1)
| ~ incident(X2,X0)
| ~ incident(X2,X1)
| ~ incident(X3,X0)
| ~ incident(X3,X1) ),
inference(flattening,[],[f50]) ).
fof(f52,plain,
! [X0,X1] :
( ? [X2] :
( incident(X0,X2)
& incident(X1,X2) )
| ~ point_equal(X0,X0)
| ~ point_equal(X1,X1) ),
inference(ennf_transformation,[],[f22]) ).
fof(f53,plain,
! [X0,X1] :
( ? [X2] :
( incident(X0,X2)
& incident(X1,X2) )
| ~ point_equal(X0,X0)
| ~ point_equal(X1,X1) ),
inference(flattening,[],[f52]) ).
fof(f56,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
( colinear(X6,X7,X8,sK0(X6,X7,X8))
| incident(X0,X10)
| incident(X1,X10)
| incident(X2,X10)
| incident(X3,X9)
| incident(X4,X9)
| incident(X5,X9)
| ~ colinear(X0,X1,X2,X9)
| ~ colinear(X3,X4,X5,X10)
| ~ colinear(X1,X5,X6,X11)
| ~ colinear(X2,X4,X6,X12)
| ~ colinear(X1,X3,X7,X13)
| ~ colinear(X0,X4,X7,X14)
| ~ colinear(X2,X3,X8,X15)
| ~ colinear(X0,X5,X8,X16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X17,sK0(X6,X7,X8))],[f49]) ).
fof(f57,plain,
! [X0,X1] :
( ( incident(X0,sK1(X0,X1))
& incident(X1,sK1(X0,X1)) )
| ~ point_equal(X0,X0)
| ~ point_equal(X1,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f53]) ).
fof(f60,plain,
colinear(d,e,f,m),
inference(cnf_transformation,[],[f1]) ).
fof(f61,plain,
colinear(a,b,c,l),
inference(cnf_transformation,[],[f1]) ).
fof(f62,plain,
colinear(c,e,g,o),
inference(cnf_transformation,[],[f2]) ).
fof(f63,plain,
colinear(b,f,g,n),
inference(cnf_transformation,[],[f2]) ).
fof(f64,plain,
colinear(a,e,h,q),
inference(cnf_transformation,[],[f3]) ).
fof(f65,plain,
colinear(b,d,h,p),
inference(cnf_transformation,[],[f3]) ).
fof(f66,plain,
colinear(a,f,i,s),
inference(cnf_transformation,[],[f4]) ).
fof(f67,plain,
colinear(c,d,i,r),
inference(cnf_transformation,[],[f4]) ).
fof(f68,plain,
( goal
| ~ line_equal(n,o) ),
inference(cnf_transformation,[],[f28]) ).
fof(f69,plain,
( goal
| ~ line_equal(p,q) ),
inference(cnf_transformation,[],[f29]) ).
fof(f70,plain,
( goal
| ~ line_equal(s,r) ),
inference(cnf_transformation,[],[f30]) ).
fof(f71,plain,
! [X0] :
( goal
| ~ line_equal(X0,X0)
| ~ incident(g,X0)
| ~ incident(h,X0)
| ~ incident(i,X0) ),
inference(cnf_transformation,[],[f32]) ).
fof(f72,plain,
! [X2,X3,X0,X1] :
( ~ colinear(X0,X1,X2,X3)
| incident(X0,X3) ),
inference(cnf_transformation,[],[f33]) ).
fof(f73,plain,
! [X2,X3,X0,X1] :
( ~ colinear(X0,X1,X2,X3)
| incident(X1,X3) ),
inference(cnf_transformation,[],[f34]) ).
fof(f74,plain,
! [X2,X3,X0,X1] :
( ~ colinear(X0,X1,X2,X3)
| incident(X2,X3) ),
inference(cnf_transformation,[],[f35]) ).
fof(f75,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| point_equal(X0,X0) ),
inference(cnf_transformation,[],[f36]) ).
fof(f76,plain,
! [X0,X1] :
( ~ point_equal(X0,X1)
| point_equal(X1,X0) ),
inference(cnf_transformation,[],[f37]) ).
fof(f77,plain,
! [X2,X0,X1] :
( ~ point_equal(X1,X2)
| ~ point_equal(X0,X1)
| point_equal(X0,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f78,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| line_equal(X1,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f79,plain,
! [X0,X1] :
( ~ line_equal(X0,X1)
| line_equal(X1,X0) ),
inference(cnf_transformation,[],[f41]) ).
fof(f80,plain,
! [X2,X0,X1] :
( ~ line_equal(X1,X2)
| ~ line_equal(X0,X1)
| line_equal(X0,X2) ),
inference(cnf_transformation,[],[f43]) ).
fof(f81,plain,
! [X2,X0,X1] :
( ~ point_equal(X0,X1)
| incident(X0,X2)
| ~ incident(X1,X2) ),
inference(cnf_transformation,[],[f45]) ).
fof(f82,plain,
! [X2,X0,X1] :
( ~ incident(X0,X1)
| incident(X0,X2)
| ~ line_equal(X1,X2) ),
inference(cnf_transformation,[],[f47]) ).
fof(f83,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ colinear(X3,X4,X5,X10)
| incident(X0,X10)
| incident(X1,X10)
| incident(X2,X10)
| incident(X3,X9)
| incident(X4,X9)
| incident(X5,X9)
| ~ colinear(X0,X1,X2,X9)
| colinear(X6,X7,X8,sK0(X6,X7,X8))
| ~ colinear(X1,X5,X6,X11)
| ~ colinear(X2,X4,X6,X12)
| ~ colinear(X1,X3,X7,X13)
| ~ colinear(X0,X4,X7,X14)
| ~ colinear(X2,X3,X8,X15)
| ~ colinear(X0,X5,X8,X16) ),
inference(cnf_transformation,[],[f56]) ).
fof(f84,plain,
! [X2,X3,X0,X1] :
( ~ incident(X3,X1)
| line_equal(X0,X1)
| ~ incident(X2,X0)
| ~ incident(X2,X1)
| ~ incident(X3,X0)
| point_equal(X2,X3) ),
inference(cnf_transformation,[],[f51]) ).
fof(f85,plain,
! [X0,X1] :
( ~ point_equal(X1,X1)
| ~ point_equal(X0,X0)
| incident(X1,sK1(X0,X1)) ),
inference(cnf_transformation,[],[f57]) ).
fof(f86,plain,
! [X0,X1] :
( ~ point_equal(X1,X1)
| ~ point_equal(X0,X0)
| incident(X0,sK1(X0,X1)) ),
inference(cnf_transformation,[],[f57]) ).
fof(f89,plain,
~ goal,
inference(cnf_transformation,[],[f27]) ).
fof(f90,plain,
! [X0] :
( ~ line_equal(X0,X0)
| ~ incident(g,X0)
| ~ incident(h,X0)
| ~ incident(i,X0) ),
inference(forward_subsumption_resolution,[],[f71,f89]) ).
fof(f91,plain,
~ line_equal(s,r),
inference(forward_subsumption_resolution,[],[f70,f89]) ).
fof(f92,plain,
~ line_equal(p,q),
inference(forward_subsumption_resolution,[],[f69,f89]) ).
fof(f93,plain,
~ line_equal(n,o),
inference(forward_subsumption_resolution,[],[f68,f89]) ).
fof(f94,plain,
! [X0] :
( ~ incident(i,X0)
| ~ incident(h,X0)
| ~ incident(g,X0) ),
inference(forward_subsumption_resolution,[],[f90,f78]) ).
fof(f95,plain,
incident(c,l),
inference(resolution,[],[f61,f74]) ).
fof(f96,plain,
incident(b,l),
inference(resolution,[],[f61,f73]) ).
fof(f97,plain,
incident(a,l),
inference(resolution,[],[f61,f72]) ).
fof(f98,plain,
! [X0] :
( ~ line_equal(l,X0)
| incident(a,X0) ),
inference(resolution,[],[f97,f82]) ).
fof(f101,plain,
! [X0] :
( ~ line_equal(l,X0)
| incident(b,X0) ),
inference(resolution,[],[f96,f82]) ).
fof(f102,plain,
point_equal(b,b),
inference(resolution,[],[f96,f75]) ).
fof(f104,plain,
! [X0] :
( ~ line_equal(l,X0)
| incident(c,X0) ),
inference(resolution,[],[f95,f82]) ).
fof(f107,plain,
incident(f,m),
inference(resolution,[],[f60,f74]) ).
fof(f108,plain,
incident(e,m),
inference(resolution,[],[f60,f73]) ).
fof(f109,plain,
incident(d,m),
inference(resolution,[],[f60,f72]) ).
fof(f110,plain,
! [X0] :
( ~ line_equal(m,X0)
| incident(f,X0) ),
inference(resolution,[],[f107,f82]) ).
fof(f113,plain,
! [X0] :
( ~ line_equal(m,X0)
| incident(e,X0) ),
inference(resolution,[],[f108,f82]) ).
fof(f114,plain,
point_equal(e,e),
inference(resolution,[],[f108,f75]) ).
fof(f116,plain,
! [X0] :
( ~ line_equal(m,X0)
| incident(d,X0) ),
inference(resolution,[],[f109,f82]) ).
fof(f119,plain,
incident(g,n),
inference(resolution,[],[f63,f74]) ).
fof(f120,plain,
incident(f,n),
inference(resolution,[],[f63,f73]) ).
fof(f121,plain,
incident(b,n),
inference(resolution,[],[f63,f72]) ).
fof(f122,plain,
! [X0] :
( ~ line_equal(n,X0)
| incident(f,X0) ),
inference(resolution,[],[f120,f82]) ).
fof(f125,plain,
! [X0] :
( ~ line_equal(n,X0)
| incident(b,X0) ),
inference(resolution,[],[f121,f82]) ).
fof(f128,plain,
! [X0] :
( ~ line_equal(n,X0)
| incident(g,X0) ),
inference(resolution,[],[f119,f82]) ).
fof(f129,plain,
point_equal(g,g),
inference(resolution,[],[f119,f75]) ).
fof(f131,plain,
incident(h,q),
inference(resolution,[],[f64,f74]) ).
fof(f132,plain,
incident(e,q),
inference(resolution,[],[f64,f73]) ).
fof(f133,plain,
incident(a,q),
inference(resolution,[],[f64,f72]) ).
fof(f134,plain,
! [X0] :
( ~ line_equal(q,X0)
| incident(e,X0) ),
inference(resolution,[],[f132,f82]) ).
fof(f137,plain,
! [X0] :
( ~ line_equal(q,X0)
| incident(h,X0) ),
inference(resolution,[],[f131,f82]) ).
fof(f138,plain,
point_equal(h,h),
inference(resolution,[],[f131,f75]) ).
fof(f143,plain,
! [X0,X1] :
( ~ incident(a,X0)
| ~ incident(X1,X0)
| ~ incident(X1,l)
| line_equal(X0,l)
| point_equal(X1,a) ),
inference(resolution,[],[f84,f97]) ).
fof(f144,plain,
! [X0,X1] :
( ~ incident(b,X0)
| ~ incident(X1,X0)
| ~ incident(X1,l)
| line_equal(X0,l)
| point_equal(X1,b) ),
inference(resolution,[],[f84,f96]) ).
fof(f145,plain,
! [X0,X1] :
( ~ incident(c,X0)
| ~ incident(X1,X0)
| ~ incident(X1,l)
| line_equal(X0,l)
| point_equal(X1,c) ),
inference(resolution,[],[f84,f95]) ).
fof(f146,plain,
! [X0,X1] :
( ~ incident(f,X0)
| ~ incident(X1,X0)
| ~ incident(X1,m)
| line_equal(X0,m)
| point_equal(X1,f) ),
inference(resolution,[],[f84,f107]) ).
fof(f147,plain,
! [X0,X1] :
( ~ incident(e,X0)
| ~ incident(X1,X0)
| ~ incident(X1,m)
| line_equal(X0,m)
| point_equal(X1,e) ),
inference(resolution,[],[f84,f108]) ).
fof(f148,plain,
! [X0,X1] :
( ~ incident(d,X0)
| ~ incident(X1,X0)
| ~ incident(X1,m)
| line_equal(X0,m)
| point_equal(X1,d) ),
inference(resolution,[],[f84,f109]) ).
fof(f149,plain,
! [X0,X1] :
( ~ incident(f,X0)
| ~ incident(X1,X0)
| ~ incident(X1,n)
| line_equal(X0,n)
| point_equal(X1,f) ),
inference(resolution,[],[f84,f120]) ).
fof(f151,plain,
! [X0,X1] :
( ~ incident(g,X0)
| ~ incident(X1,X0)
| ~ incident(X1,n)
| line_equal(X0,n)
| point_equal(X1,g) ),
inference(resolution,[],[f84,f119]) ).
fof(f152,plain,
! [X0,X1] :
( ~ incident(e,X0)
| ~ incident(X1,X0)
| ~ incident(X1,q)
| line_equal(X0,q)
| point_equal(X1,e) ),
inference(resolution,[],[f84,f132]) ).
fof(f156,plain,
! [X0] :
( ~ incident(X0,n)
| ~ incident(X0,m)
| line_equal(n,m)
| point_equal(X0,f) ),
inference(resolution,[],[f146,f120]) ).
fof(f159,definition,
( spl3_1
<=> line_equal(n,m) ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
fof(f160,plain,
( ~ line_equal(n,m)
| spl3_1 ),
inference(avatar_component_clause,[],[f159]) ).
fof(f161,plain,
( line_equal(n,m)
| ~ spl3_1 ),
inference(avatar_component_clause,[],[f159]) ).
fof(f163,definition,
( spl3_2
<=> ! [X0] :
( ~ incident(X0,n)
| point_equal(X0,f)
| ~ incident(X0,m) ) ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f164,plain,
( ! [X0] :
( ~ incident(X0,n)
| point_equal(X0,f)
| ~ incident(X0,m) )
| ~ spl3_2 ),
inference(avatar_component_clause,[],[f163]) ).
fof(f165,plain,
( spl3_1
| spl3_2 ),
inference(avatar_split_clause,[],[f156,f163,f159]) ).
fof(f168,plain,
( point_equal(g,f)
| ~ incident(g,m)
| ~ spl3_2 ),
inference(resolution,[],[f164,f119]) ).
fof(f170,definition,
( spl3_3
<=> incident(g,m) ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f171,plain,
( incident(g,m)
| ~ spl3_3 ),
inference(avatar_component_clause,[],[f170]) ).
fof(f172,plain,
( ~ incident(g,m)
| spl3_3 ),
inference(avatar_component_clause,[],[f170]) ).
fof(f174,definition,
( spl3_4
<=> point_equal(g,f) ),
introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition]) ).
fof(f175,plain,
( ~ point_equal(g,f)
| spl3_4 ),
inference(avatar_component_clause,[],[f174]) ).
fof(f176,plain,
( point_equal(g,f)
| ~ spl3_4 ),
inference(avatar_component_clause,[],[f174]) ).
fof(f179,definition,
( spl3_5
<=> incident(b,m) ),
introduced(definition,[new_symbols(definition,[spl3_5])],[avatar_definition]) ).
fof(f180,plain,
( incident(b,m)
| ~ spl3_5 ),
inference(avatar_component_clause,[],[f179]) ).
fof(f181,plain,
( ~ incident(b,m)
| spl3_5 ),
inference(avatar_component_clause,[],[f179]) ).
fof(f183,definition,
( spl3_6
<=> point_equal(b,f) ),
introduced(definition,[new_symbols(definition,[spl3_6])],[avatar_definition]) ).
fof(f184,plain,
( ~ point_equal(b,f)
| spl3_6 ),
inference(avatar_component_clause,[],[f183]) ).
fof(f185,plain,
( point_equal(b,f)
| ~ spl3_6 ),
inference(avatar_component_clause,[],[f183]) ).
fof(f188,plain,
! [X0] :
( ~ incident(X0,q)
| ~ incident(X0,m)
| line_equal(q,m)
| point_equal(X0,e) ),
inference(resolution,[],[f147,f132]) ).
fof(f191,definition,
( spl3_7
<=> line_equal(q,m) ),
introduced(definition,[new_symbols(definition,[spl3_7])],[avatar_definition]) ).
fof(f193,plain,
( line_equal(q,m)
| ~ spl3_7 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f195,definition,
( spl3_8
<=> ! [X0] :
( ~ incident(X0,q)
| point_equal(X0,e)
| ~ incident(X0,m) ) ),
introduced(definition,[new_symbols(definition,[spl3_8])],[avatar_definition]) ).
fof(f196,plain,
( ! [X0] :
( ~ incident(X0,q)
| point_equal(X0,e)
| ~ incident(X0,m) )
| ~ spl3_8 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f197,plain,
( spl3_7
| spl3_8 ),
inference(avatar_split_clause,[],[f188,f195,f191]) ).
fof(f198,plain,
( incident(h,m)
| ~ spl3_7 ),
inference(resolution,[],[f193,f137]) ).
fof(f206,plain,
! [X0] :
( incident(X0,sK1(X0,h))
| ~ point_equal(X0,X0) ),
inference(resolution,[],[f138,f86]) ).
fof(f207,plain,
! [X0] :
( ~ point_equal(X0,X0)
| incident(h,sK1(X0,h)) ),
inference(resolution,[],[f138,f85]) ).
fof(f215,plain,
( ~ point_equal(i,i)
| ~ incident(h,sK1(i,h))
| ~ incident(g,sK1(i,h)) ),
inference(resolution,[],[f206,f94]) ).
fof(f216,plain,
( ~ point_equal(i,i)
| ~ incident(g,sK1(i,h)) ),
inference(forward_subsumption_resolution,[],[f215,f207]) ).
fof(f221,definition,
( spl3_9
<=> incident(g,sK1(i,h)) ),
introduced(definition,[new_symbols(definition,[spl3_9])],[avatar_definition]) ).
fof(f223,plain,
( ~ incident(g,sK1(i,h))
| spl3_9 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f225,definition,
( spl3_10
<=> point_equal(i,i) ),
introduced(definition,[new_symbols(definition,[spl3_10])],[avatar_definition]) ).
fof(f226,plain,
( point_equal(i,i)
| ~ spl3_10 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f227,plain,
( ~ point_equal(i,i)
| spl3_10 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f228,plain,
( ~ spl3_9
| ~ spl3_10 ),
inference(avatar_split_clause,[],[f216,f225,f221]) ).
fof(f257,plain,
incident(g,o),
inference(resolution,[],[f62,f74]) ).
fof(f258,plain,
incident(e,o),
inference(resolution,[],[f62,f73]) ).
fof(f259,plain,
incident(c,o),
inference(resolution,[],[f62,f72]) ).
fof(f260,plain,
! [X0] :
( ~ incident(X0,o)
| ~ incident(X0,m)
| line_equal(o,m)
| point_equal(X0,e) ),
inference(resolution,[],[f258,f147]) ).
fof(f261,plain,
! [X0,X1] :
( ~ incident(e,X0)
| ~ incident(X1,X0)
| ~ incident(X1,o)
| line_equal(X0,o)
| point_equal(X1,e) ),
inference(resolution,[],[f258,f84]) ).
fof(f266,definition,
( spl3_17
<=> line_equal(o,m) ),
introduced(definition,[new_symbols(definition,[spl3_17])],[avatar_definition]) ).
fof(f268,plain,
( line_equal(o,m)
| ~ spl3_17 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f270,definition,
( spl3_18
<=> ! [X0] :
( ~ incident(X0,o)
| point_equal(X0,e)
| ~ incident(X0,m) ) ),
introduced(definition,[new_symbols(definition,[spl3_18])],[avatar_definition]) ).
fof(f271,plain,
( ! [X0] :
( ~ incident(X0,o)
| point_equal(X0,e)
| ~ incident(X0,m) )
| ~ spl3_18 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f272,plain,
( spl3_17
| spl3_18 ),
inference(avatar_split_clause,[],[f260,f270,f266]) ).
fof(f277,plain,
! [X0,X1] :
( ~ incident(g,X0)
| ~ incident(X1,X0)
| ~ incident(X1,o)
| line_equal(X0,o)
| point_equal(X1,g) ),
inference(resolution,[],[f257,f84]) ).
fof(f278,plain,
! [X0] :
( ~ line_equal(o,X0)
| incident(g,X0) ),
inference(resolution,[],[f257,f82]) ).
fof(f281,plain,
( incident(g,m)
| ~ spl3_17 ),
inference(resolution,[],[f268,f278]) ).
fof(f286,plain,
( $false
| spl3_3
| ~ spl3_17 ),
inference(forward_subsumption_resolution,[],[f281,f172]) ).
fof(f287,plain,
( spl3_3
| ~ spl3_17 ),
inference(avatar_contradiction_clause,[],[f286]) ).
fof(f293,plain,
( incident(b,m)
| ~ spl3_1 ),
inference(resolution,[],[f161,f125]) ).
fof(f296,plain,
( line_equal(m,n)
| ~ spl3_1 ),
inference(resolution,[],[f161,f79]) ).
fof(f299,plain,
( point_equal(g,f)
| ~ spl3_2
| ~ spl3_3 ),
inference(forward_subsumption_resolution,[],[f168,f171]) ).
fof(f300,plain,
( ! [X0] :
( ~ incident(f,X0)
| incident(g,X0) )
| ~ spl3_4 ),
inference(resolution,[],[f176,f81]) ).
fof(f302,plain,
( point_equal(f,g)
| ~ spl3_4 ),
inference(resolution,[],[f176,f76]) ).
fof(f303,plain,
( incident(g,m)
| ~ spl3_4 ),
inference(resolution,[],[f300,f107]) ).
fof(f308,plain,
( point_equal(b,f)
| ~ incident(b,m)
| ~ spl3_2 ),
inference(resolution,[],[f164,f121]) ).
fof(f310,plain,
( ! [X0] :
( ~ incident(g,X0)
| incident(f,X0) )
| ~ spl3_4 ),
inference(resolution,[],[f302,f81]) ).
fof(f315,plain,
( incident(f,o)
| ~ spl3_4 ),
inference(resolution,[],[f310,f257]) ).
fof(f318,plain,
! [X0] :
( ~ incident(X0,m)
| ~ incident(X0,o)
| line_equal(m,o)
| point_equal(X0,e) ),
inference(resolution,[],[f261,f108]) ).
fof(f351,plain,
! [X0] :
( ~ incident(X0,o)
| ~ incident(X0,l)
| line_equal(o,l)
| point_equal(X0,c) ),
inference(resolution,[],[f145,f259]) ).
fof(f356,definition,
( spl3_23
<=> line_equal(o,l) ),
introduced(definition,[new_symbols(definition,[spl3_23])],[avatar_definition]) ).
fof(f358,plain,
( line_equal(o,l)
| ~ spl3_23 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f360,definition,
( spl3_24
<=> ! [X0] :
( ~ incident(X0,o)
| point_equal(X0,c)
| ~ incident(X0,l) ) ),
introduced(definition,[new_symbols(definition,[spl3_24])],[avatar_definition]) ).
fof(f361,plain,
( ! [X0] :
( ~ incident(X0,o)
| point_equal(X0,c)
| ~ incident(X0,l) )
| ~ spl3_24 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f362,plain,
( spl3_23
| spl3_24 ),
inference(avatar_split_clause,[],[f351,f360,f356]) ).
fof(f371,plain,
( incident(g,l)
| ~ spl3_23 ),
inference(resolution,[],[f358,f278]) ).
fof(f377,plain,
! [X0] :
( ~ incident(X0,n)
| ~ incident(X0,l)
| line_equal(n,l)
| point_equal(X0,b) ),
inference(resolution,[],[f144,f121]) ).
fof(f382,definition,
( spl3_27
<=> line_equal(n,l) ),
introduced(definition,[new_symbols(definition,[spl3_27])],[avatar_definition]) ).
fof(f384,plain,
( line_equal(n,l)
| ~ spl3_27 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f386,definition,
( spl3_28
<=> ! [X0] :
( ~ incident(X0,n)
| point_equal(X0,b)
| ~ incident(X0,l) ) ),
introduced(definition,[new_symbols(definition,[spl3_28])],[avatar_definition]) ).
fof(f387,plain,
( ! [X0] :
( ~ incident(X0,n)
| point_equal(X0,b)
| ~ incident(X0,l) )
| ~ spl3_28 ),
inference(avatar_component_clause,[],[f386]) ).
fof(f388,plain,
( spl3_27
| spl3_28 ),
inference(avatar_split_clause,[],[f377,f386,f382]) ).
fof(f397,plain,
( incident(g,l)
| ~ spl3_27 ),
inference(resolution,[],[f384,f128]) ).
fof(f399,plain,
( incident(f,l)
| ~ spl3_27 ),
inference(resolution,[],[f384,f122]) ).
fof(f401,plain,
( line_equal(l,n)
| ~ spl3_27 ),
inference(resolution,[],[f384,f79]) ).
fof(f406,plain,
! [X0] :
( incident(X0,sK1(X0,g))
| ~ point_equal(X0,X0) ),
inference(resolution,[],[f129,f86]) ).
fof(f407,plain,
! [X0] :
( ~ point_equal(X0,X0)
| incident(g,sK1(X0,g)) ),
inference(resolution,[],[f129,f85]) ).
fof(f422,plain,
( ~ point_equal(i,i)
| ~ incident(h,sK1(i,g))
| ~ incident(g,sK1(i,g)) ),
inference(resolution,[],[f406,f94]) ).
fof(f423,plain,
( ~ point_equal(i,i)
| ~ incident(h,sK1(i,g)) ),
inference(forward_subsumption_resolution,[],[f422,f407]) ).
fof(f433,definition,
( spl3_31
<=> incident(h,sK1(i,g)) ),
introduced(definition,[new_symbols(definition,[spl3_31])],[avatar_definition]) ).
fof(f435,plain,
( ~ incident(h,sK1(i,g))
| spl3_31 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f436,plain,
( ~ spl3_31
| ~ spl3_10 ),
inference(avatar_split_clause,[],[f423,f225,f433]) ).
fof(f508,plain,
incident(h,p),
inference(resolution,[],[f65,f74]) ).
fof(f509,plain,
incident(d,p),
inference(resolution,[],[f65,f73]) ).
fof(f510,plain,
incident(b,p),
inference(resolution,[],[f65,f72]) ).
fof(f511,plain,
! [X0,X1] :
( ~ incident(h,X0)
| ~ incident(X1,X0)
| ~ incident(X1,p)
| line_equal(X0,p)
| point_equal(X1,h) ),
inference(resolution,[],[f508,f84]) ).
fof(f512,plain,
! [X0] :
( ~ line_equal(p,X0)
| incident(h,X0) ),
inference(resolution,[],[f508,f82]) ).
fof(f515,plain,
! [X0] :
( ~ incident(X0,p)
| ~ incident(X0,l)
| line_equal(p,l)
| point_equal(X0,b) ),
inference(resolution,[],[f510,f144]) ).
fof(f516,plain,
! [X0,X1] :
( ~ incident(b,X0)
| ~ incident(X1,X0)
| ~ incident(X1,p)
| line_equal(X0,p)
| point_equal(X1,b) ),
inference(resolution,[],[f510,f84]) ).
fof(f517,plain,
! [X0] :
( ~ line_equal(p,X0)
| incident(b,X0) ),
inference(resolution,[],[f510,f82]) ).
fof(f521,definition,
( spl3_48
<=> line_equal(p,l) ),
introduced(definition,[new_symbols(definition,[spl3_48])],[avatar_definition]) ).
fof(f523,plain,
( line_equal(p,l)
| ~ spl3_48 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f525,definition,
( spl3_49
<=> ! [X0] :
( ~ incident(X0,p)
| point_equal(X0,b)
| ~ incident(X0,l) ) ),
introduced(definition,[new_symbols(definition,[spl3_49])],[avatar_definition]) ).
fof(f526,plain,
( ! [X0] :
( ~ incident(X0,p)
| point_equal(X0,b)
| ~ incident(X0,l) )
| ~ spl3_49 ),
inference(avatar_component_clause,[],[f525]) ).
fof(f527,plain,
( spl3_48
| spl3_49 ),
inference(avatar_split_clause,[],[f515,f525,f521]) ).
fof(f528,plain,
! [X0] :
( ~ incident(X0,p)
| ~ incident(X0,m)
| line_equal(p,m)
| point_equal(X0,d) ),
inference(resolution,[],[f509,f148]) ).
fof(f534,definition,
( spl3_50
<=> line_equal(p,m) ),
introduced(definition,[new_symbols(definition,[spl3_50])],[avatar_definition]) ).
fof(f536,plain,
( line_equal(p,m)
| ~ spl3_50 ),
inference(avatar_component_clause,[],[f534]) ).
fof(f538,definition,
( spl3_51
<=> ! [X0] :
( ~ incident(X0,p)
| point_equal(X0,d)
| ~ incident(X0,m) ) ),
introduced(definition,[new_symbols(definition,[spl3_51])],[avatar_definition]) ).
fof(f539,plain,
( ! [X0] :
( ~ incident(X0,p)
| point_equal(X0,d)
| ~ incident(X0,m) )
| ~ spl3_51 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f540,plain,
( spl3_50
| spl3_51 ),
inference(avatar_split_clause,[],[f528,f538,f534]) ).
fof(f543,plain,
( incident(b,m)
| ~ spl3_50 ),
inference(resolution,[],[f536,f517]) ).
fof(f546,plain,
( $false
| spl3_5
| ~ spl3_50 ),
inference(forward_subsumption_resolution,[],[f543,f181]) ).
fof(f547,plain,
( spl3_5
| ~ spl3_50 ),
inference(avatar_contradiction_clause,[],[f546]) ).
fof(f548,plain,
( spl3_5
| ~ spl3_1 ),
inference(avatar_split_clause,[],[f293,f159,f179]) ).
fof(f549,plain,
( ! [X0] :
( ~ incident(X0,m)
| ~ incident(X0,l)
| line_equal(m,l)
| point_equal(X0,b) )
| ~ spl3_5 ),
inference(resolution,[],[f180,f144]) ).
fof(f555,definition,
( spl3_52
<=> line_equal(m,l) ),
introduced(definition,[new_symbols(definition,[spl3_52])],[avatar_definition]) ).
fof(f557,plain,
( line_equal(m,l)
| ~ spl3_52 ),
inference(avatar_component_clause,[],[f555]) ).
fof(f559,definition,
( spl3_53
<=> ! [X0] :
( ~ incident(X0,m)
| point_equal(X0,b)
| ~ incident(X0,l) ) ),
introduced(definition,[new_symbols(definition,[spl3_53])],[avatar_definition]) ).
fof(f560,plain,
( ! [X0] :
( ~ incident(X0,m)
| point_equal(X0,b)
| ~ incident(X0,l) )
| ~ spl3_53 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f561,plain,
( spl3_52
| spl3_53
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f549,f179,f559,f555]) ).
fof(f564,plain,
( incident(h,l)
| ~ spl3_48 ),
inference(resolution,[],[f523,f512]) ).
fof(f573,plain,
( incident(c,n)
| ~ spl3_27 ),
inference(resolution,[],[f401,f104]) ).
fof(f600,plain,
! [X0] :
( ~ incident(X0,l)
| ~ incident(X0,p)
| line_equal(l,p)
| point_equal(X0,b) ),
inference(resolution,[],[f516,f96]) ).
fof(f601,plain,
! [X0] :
( ~ incident(X0,n)
| ~ incident(X0,p)
| line_equal(n,p)
| point_equal(X0,b) ),
inference(resolution,[],[f516,f121]) ).
fof(f609,definition,
( spl3_58
<=> line_equal(n,p) ),
introduced(definition,[new_symbols(definition,[spl3_58])],[avatar_definition]) ).
fof(f611,plain,
( line_equal(n,p)
| ~ spl3_58 ),
inference(avatar_component_clause,[],[f609]) ).
fof(f613,definition,
( spl3_59
<=> ! [X0] :
( ~ incident(X0,n)
| point_equal(X0,b)
| ~ incident(X0,p) ) ),
introduced(definition,[new_symbols(definition,[spl3_59])],[avatar_definition]) ).
fof(f614,plain,
( ! [X0] :
( ~ incident(X0,p)
| point_equal(X0,b)
| ~ incident(X0,n) )
| ~ spl3_59 ),
inference(avatar_component_clause,[],[f613]) ).
fof(f615,plain,
( spl3_58
| spl3_59 ),
inference(avatar_split_clause,[],[f601,f613,f609]) ).
fof(f632,plain,
( incident(g,p)
| ~ spl3_58 ),
inference(resolution,[],[f611,f128]) ).
fof(f643,plain,
! [X0] :
( ~ incident(X0,n)
| ~ incident(X0,o)
| line_equal(n,o)
| point_equal(X0,g) ),
inference(resolution,[],[f277,f119]) ).
fof(f650,plain,
! [X0] :
( ~ incident(X0,o)
| ~ incident(X0,n)
| point_equal(X0,g) ),
inference(forward_subsumption_resolution,[],[f643,f93]) ).
fof(f667,plain,
( ~ incident(e,n)
| point_equal(e,g) ),
inference(resolution,[],[f650,f258]) ).
fof(f668,plain,
( ~ incident(c,n)
| point_equal(c,g) ),
inference(resolution,[],[f650,f259]) ).
fof(f670,plain,
( point_equal(c,g)
| ~ spl3_27 ),
inference(forward_subsumption_resolution,[],[f668,f573]) ).
fof(f672,definition,
( spl3_68
<=> point_equal(e,g) ),
introduced(definition,[new_symbols(definition,[spl3_68])],[avatar_definition]) ).
fof(f674,plain,
( point_equal(e,g)
| ~ spl3_68 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f676,definition,
( spl3_69
<=> incident(e,n) ),
introduced(definition,[new_symbols(definition,[spl3_69])],[avatar_definition]) ).
fof(f678,plain,
( ~ incident(e,n)
| spl3_69 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f679,plain,
( spl3_68
| ~ spl3_69 ),
inference(avatar_split_clause,[],[f667,f676,f672]) ).
fof(f682,plain,
( point_equal(g,c)
| ~ spl3_27 ),
inference(resolution,[],[f670,f76]) ).
fof(f699,plain,
! [X0] :
( ~ incident(X0,q)
| ~ incident(X0,l)
| line_equal(q,l)
| point_equal(X0,a) ),
inference(resolution,[],[f143,f133]) ).
fof(f706,definition,
( spl3_70
<=> line_equal(q,l) ),
introduced(definition,[new_symbols(definition,[spl3_70])],[avatar_definition]) ).
fof(f708,plain,
( line_equal(q,l)
| ~ spl3_70 ),
inference(avatar_component_clause,[],[f706]) ).
fof(f710,definition,
( spl3_71
<=> ! [X0] :
( ~ incident(X0,q)
| point_equal(X0,a)
| ~ incident(X0,l) ) ),
introduced(definition,[new_symbols(definition,[spl3_71])],[avatar_definition]) ).
fof(f711,plain,
( ! [X0] :
( ~ incident(X0,q)
| point_equal(X0,a)
| ~ incident(X0,l) )
| ~ spl3_71 ),
inference(avatar_component_clause,[],[f710]) ).
fof(f712,plain,
( spl3_70
| spl3_71 ),
inference(avatar_split_clause,[],[f699,f710,f706]) ).
fof(f731,plain,
( incident(e,l)
| ~ spl3_70 ),
inference(resolution,[],[f708,f134]) ).
fof(f733,plain,
( line_equal(l,q)
| ~ spl3_70 ),
inference(resolution,[],[f708,f79]) ).
fof(f736,plain,
! [X0] :
( ~ incident(X0,q)
| ~ incident(X0,p)
| line_equal(q,p)
| point_equal(X0,h) ),
inference(resolution,[],[f511,f131]) ).
fof(f743,definition,
( spl3_76
<=> line_equal(q,p) ),
introduced(definition,[new_symbols(definition,[spl3_76])],[avatar_definition]) ).
fof(f745,plain,
( line_equal(q,p)
| ~ spl3_76 ),
inference(avatar_component_clause,[],[f743]) ).
fof(f747,definition,
( spl3_77
<=> ! [X0] :
( ~ incident(X0,q)
| point_equal(X0,h)
| ~ incident(X0,p) ) ),
introduced(definition,[new_symbols(definition,[spl3_77])],[avatar_definition]) ).
fof(f748,plain,
( ! [X0] :
( ~ incident(X0,q)
| point_equal(X0,h)
| ~ incident(X0,p) )
| ~ spl3_77 ),
inference(avatar_component_clause,[],[f747]) ).
fof(f749,plain,
( spl3_76
| spl3_77 ),
inference(avatar_split_clause,[],[f736,f747,f743]) ).
fof(f770,plain,
( line_equal(p,q)
| ~ spl3_76 ),
inference(resolution,[],[f745,f79]) ).
fof(f771,plain,
( $false
| ~ spl3_76 ),
inference(forward_subsumption_resolution,[],[f770,f92]) ).
fof(f772,plain,
~ spl3_76,
inference(avatar_contradiction_clause,[],[f771]) ).
fof(f930,plain,
( point_equal(e,h)
| ~ incident(e,p)
| ~ spl3_77 ),
inference(resolution,[],[f748,f132]) ).
fof(f932,plain,
( point_equal(a,h)
| ~ incident(a,p)
| ~ spl3_77 ),
inference(resolution,[],[f748,f133]) ).
fof(f934,definition,
( spl3_106
<=> incident(a,p) ),
introduced(definition,[new_symbols(definition,[spl3_106])],[avatar_definition]) ).
fof(f936,plain,
( ~ incident(a,p)
| spl3_106 ),
inference(avatar_component_clause,[],[f934]) ).
fof(f938,definition,
( spl3_107
<=> point_equal(a,h) ),
introduced(definition,[new_symbols(definition,[spl3_107])],[avatar_definition]) ).
fof(f940,plain,
( point_equal(a,h)
| ~ spl3_107 ),
inference(avatar_component_clause,[],[f938]) ).
fof(f941,plain,
( ~ spl3_106
| spl3_107
| ~ spl3_77 ),
inference(avatar_split_clause,[],[f932,f747,f938,f934]) ).
fof(f943,definition,
( spl3_108
<=> incident(e,p) ),
introduced(definition,[new_symbols(definition,[spl3_108])],[avatar_definition]) ).
fof(f945,plain,
( ~ incident(e,p)
| spl3_108 ),
inference(avatar_component_clause,[],[f943]) ).
fof(f947,definition,
( spl3_109
<=> point_equal(e,h) ),
introduced(definition,[new_symbols(definition,[spl3_109])],[avatar_definition]) ).
fof(f949,plain,
( point_equal(e,h)
| ~ spl3_109 ),
inference(avatar_component_clause,[],[f947]) ).
fof(f950,plain,
( ~ spl3_108
| spl3_109
| ~ spl3_77 ),
inference(avatar_split_clause,[],[f930,f747,f947,f943]) ).
fof(f1263,plain,
( point_equal(e,c)
| ~ incident(e,l)
| ~ spl3_24 ),
inference(resolution,[],[f361,f258]) ).
fof(f1266,plain,
( point_equal(e,c)
| ~ spl3_24
| ~ spl3_70 ),
inference(forward_subsumption_resolution,[],[f1263,f731]) ).
fof(f1287,plain,
( point_equal(f,b)
| ~ incident(f,l)
| ~ spl3_28 ),
inference(resolution,[],[f387,f120]) ).
fof(f1288,plain,
( point_equal(g,b)
| ~ incident(g,l)
| ~ spl3_28 ),
inference(resolution,[],[f387,f119]) ).
fof(f1289,plain,
( point_equal(g,b)
| ~ spl3_23
| ~ spl3_28 ),
inference(forward_subsumption_resolution,[],[f1288,f371]) ).
fof(f1291,definition,
( spl3_160
<=> incident(f,l) ),
introduced(definition,[new_symbols(definition,[spl3_160])],[avatar_definition]) ).
fof(f1292,plain,
( incident(f,l)
| ~ spl3_160 ),
inference(avatar_component_clause,[],[f1291]) ).
fof(f1293,plain,
( ~ incident(f,l)
| spl3_160 ),
inference(avatar_component_clause,[],[f1291]) ).
fof(f1295,definition,
( spl3_161
<=> point_equal(f,b) ),
introduced(definition,[new_symbols(definition,[spl3_161])],[avatar_definition]) ).
fof(f1297,plain,
( point_equal(f,b)
| ~ spl3_161 ),
inference(avatar_component_clause,[],[f1295]) ).
fof(f1299,plain,
( ! [X0] :
( ~ incident(b,X0)
| incident(g,X0) )
| ~ spl3_23
| ~ spl3_28 ),
inference(resolution,[],[f1289,f81]) ).
fof(f1304,plain,
( incident(g,p)
| ~ spl3_23
| ~ spl3_28 ),
inference(resolution,[],[f1299,f510]) ).
fof(f1503,plain,
incident(i,s),
inference(resolution,[],[f66,f74]) ).
fof(f1504,plain,
incident(f,s),
inference(resolution,[],[f66,f73]) ).
fof(f1505,plain,
incident(a,s),
inference(resolution,[],[f66,f72]) ).
fof(f1506,plain,
( ~ incident(h,s)
| ~ incident(g,s) ),
inference(resolution,[],[f1503,f94]) ).
fof(f1508,plain,
! [X0] :
( ~ line_equal(s,X0)
| incident(i,X0) ),
inference(resolution,[],[f1503,f82]) ).
fof(f1509,plain,
point_equal(i,i),
inference(resolution,[],[f1503,f75]) ).
fof(f1511,plain,
( $false
| spl3_10 ),
inference(forward_subsumption_resolution,[],[f1509,f227]) ).
fof(f1512,plain,
spl3_10,
inference(avatar_contradiction_clause,[],[f1511]) ).
fof(f1514,definition,
( spl3_188
<=> incident(g,s) ),
introduced(definition,[new_symbols(definition,[spl3_188])],[avatar_definition]) ).
fof(f1515,plain,
( incident(g,s)
| ~ spl3_188 ),
inference(avatar_component_clause,[],[f1514]) ).
fof(f1516,plain,
( ~ incident(g,s)
| spl3_188 ),
inference(avatar_component_clause,[],[f1514]) ).
fof(f1518,definition,
( spl3_189
<=> incident(h,s) ),
introduced(definition,[new_symbols(definition,[spl3_189])],[avatar_definition]) ).
fof(f1519,plain,
( incident(h,s)
| ~ spl3_189 ),
inference(avatar_component_clause,[],[f1518]) ).
fof(f1520,plain,
( ~ incident(h,s)
| spl3_189 ),
inference(avatar_component_clause,[],[f1518]) ).
fof(f1521,plain,
( ~ spl3_188
| ~ spl3_189 ),
inference(avatar_split_clause,[],[f1506,f1518,f1514]) ).
fof(f1565,plain,
( ! [X0] :
( ~ point_equal(X0,X0)
| incident(i,sK1(X0,i)) )
| ~ spl3_10 ),
inference(resolution,[],[f226,f85]) ).
fof(f1566,plain,
( ! [X0] :
( incident(X0,sK1(X0,i))
| ~ point_equal(X0,X0) )
| ~ spl3_10 ),
inference(resolution,[],[f226,f86]) ).
fof(f1567,plain,
( incident(h,sK1(i,h))
| ~ spl3_10 ),
inference(resolution,[],[f226,f207]) ).
fof(f1578,plain,
( ~ point_equal(b,b)
| incident(g,sK1(b,i))
| ~ spl3_10
| ~ spl3_23
| ~ spl3_28 ),
inference(resolution,[],[f1566,f1299]) ).
fof(f1607,plain,
( incident(g,sK1(b,i))
| ~ spl3_10
| ~ spl3_23
| ~ spl3_28 ),
inference(forward_subsumption_resolution,[],[f1578,f102]) ).
fof(f1716,plain,
( incident(i,sK1(b,i))
| ~ spl3_10 ),
inference(resolution,[],[f1565,f102]) ).
fof(f1717,plain,
( incident(i,sK1(e,i))
| ~ spl3_10 ),
inference(resolution,[],[f1565,f114]) ).
fof(f1722,plain,
( incident(g,s)
| ~ spl3_4 ),
inference(resolution,[],[f1504,f300]) ).
fof(f1723,plain,
! [X0] :
( ~ incident(X0,s)
| ~ incident(X0,m)
| line_equal(s,m)
| point_equal(X0,f) ),
inference(resolution,[],[f1504,f146]) ).
fof(f1724,plain,
! [X0,X1] :
( ~ incident(f,X0)
| ~ incident(X1,X0)
| ~ incident(X1,s)
| line_equal(X0,s)
| point_equal(X1,f) ),
inference(resolution,[],[f1504,f84]) ).
fof(f1729,definition,
( spl3_224
<=> line_equal(s,m) ),
introduced(definition,[new_symbols(definition,[spl3_224])],[avatar_definition]) ).
fof(f1731,plain,
( line_equal(s,m)
| ~ spl3_224 ),
inference(avatar_component_clause,[],[f1729]) ).
fof(f1733,definition,
( spl3_225
<=> ! [X0] :
( ~ incident(X0,s)
| point_equal(X0,f)
| ~ incident(X0,m) ) ),
introduced(definition,[new_symbols(definition,[spl3_225])],[avatar_definition]) ).
fof(f1734,plain,
( ! [X0] :
( ~ incident(X0,s)
| point_equal(X0,f)
| ~ incident(X0,m) )
| ~ spl3_225 ),
inference(avatar_component_clause,[],[f1733]) ).
fof(f1735,plain,
( spl3_224
| spl3_225 ),
inference(avatar_split_clause,[],[f1723,f1733,f1729]) ).
fof(f1752,plain,
! [X0] :
( ~ incident(X0,s)
| ~ incident(X0,l)
| line_equal(s,l)
| point_equal(X0,a) ),
inference(resolution,[],[f1505,f143]) ).
fof(f1753,plain,
! [X0,X1] :
( ~ incident(a,X0)
| ~ incident(X1,X0)
| ~ incident(X1,s)
| line_equal(X0,s)
| point_equal(X1,a) ),
inference(resolution,[],[f1505,f84]) ).
fof(f1758,definition,
( spl3_228
<=> line_equal(s,l) ),
introduced(definition,[new_symbols(definition,[spl3_228])],[avatar_definition]) ).
fof(f1760,plain,
( line_equal(s,l)
| ~ spl3_228 ),
inference(avatar_component_clause,[],[f1758]) ).
fof(f1762,definition,
( spl3_229
<=> ! [X0] :
( ~ incident(X0,s)
| point_equal(X0,a)
| ~ incident(X0,l) ) ),
introduced(definition,[new_symbols(definition,[spl3_229])],[avatar_definition]) ).
fof(f1763,plain,
( ! [X0] :
( ~ incident(X0,s)
| point_equal(X0,a)
| ~ incident(X0,l) )
| ~ spl3_229 ),
inference(avatar_component_clause,[],[f1762]) ).
fof(f1764,plain,
( spl3_228
| spl3_229 ),
inference(avatar_split_clause,[],[f1752,f1762,f1758]) ).
fof(f1770,plain,
( incident(i,m)
| ~ spl3_224 ),
inference(resolution,[],[f1731,f1508]) ).
fof(f1777,plain,
( incident(i,l)
| ~ spl3_228 ),
inference(resolution,[],[f1760,f1508]) ).
fof(f1881,definition,
( spl3_238
<=> line_equal(q,s) ),
introduced(definition,[new_symbols(definition,[spl3_238])],[avatar_definition]) ).
fof(f1883,plain,
( line_equal(q,s)
| ~ spl3_238 ),
inference(avatar_component_clause,[],[f1881]) ).
fof(f1953,plain,
( ! [X0] :
( ~ incident(X0,m)
| ~ incident(X0,p)
| line_equal(m,p)
| point_equal(X0,b) )
| ~ spl3_5 ),
inference(resolution,[],[f180,f516]) ).
fof(f1960,definition,
( spl3_256
<=> line_equal(m,p) ),
introduced(definition,[new_symbols(definition,[spl3_256])],[avatar_definition]) ).
fof(f1962,plain,
( line_equal(m,p)
| ~ spl3_256 ),
inference(avatar_component_clause,[],[f1960]) ).
fof(f1964,definition,
( spl3_257
<=> ! [X0] :
( ~ incident(X0,m)
| point_equal(X0,b)
| ~ incident(X0,p) ) ),
introduced(definition,[new_symbols(definition,[spl3_257])],[avatar_definition]) ).
fof(f1965,plain,
( ! [X0] :
( ~ incident(X0,p)
| point_equal(X0,b)
| ~ incident(X0,m) )
| ~ spl3_257 ),
inference(avatar_component_clause,[],[f1964]) ).
fof(f1966,plain,
( spl3_256
| spl3_257
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f1953,f179,f1964,f1960]) ).
fof(f1985,plain,
( incident(d,l)
| ~ spl3_52 ),
inference(resolution,[],[f557,f116]) ).
fof(f1997,definition,
( spl3_258
<=> incident(h,m) ),
introduced(definition,[new_symbols(definition,[spl3_258])],[avatar_definition]) ).
fof(f1998,plain,
( incident(h,m)
| ~ spl3_258 ),
inference(avatar_component_clause,[],[f1997]) ).
fof(f2001,definition,
( spl3_259
<=> point_equal(h,e) ),
introduced(definition,[new_symbols(definition,[spl3_259])],[avatar_definition]) ).
fof(f2003,plain,
( point_equal(h,e)
| ~ spl3_259 ),
inference(avatar_component_clause,[],[f2001]) ).
fof(f2037,plain,
( incident(d,n)
| ~ spl3_1 ),
inference(resolution,[],[f296,f116]) ).
fof(f2038,plain,
( incident(e,n)
| ~ spl3_1 ),
inference(resolution,[],[f296,f113]) ).
fof(f2047,plain,
( point_equal(b,f)
| ~ spl3_2
| ~ spl3_5 ),
inference(forward_subsumption_resolution,[],[f308,f180]) ).
fof(f2055,definition,
( spl3_260
<=> incident(a,m) ),
introduced(definition,[new_symbols(definition,[spl3_260])],[avatar_definition]) ).
fof(f2056,plain,
( incident(a,m)
| ~ spl3_260 ),
inference(avatar_component_clause,[],[f2055]) ).
fof(f2057,plain,
( ~ incident(a,m)
| spl3_260 ),
inference(avatar_component_clause,[],[f2055]) ).
fof(f2059,definition,
( spl3_261
<=> point_equal(a,e) ),
introduced(definition,[new_symbols(definition,[spl3_261])],[avatar_definition]) ).
fof(f2061,plain,
( point_equal(a,e)
| ~ spl3_261 ),
inference(avatar_component_clause,[],[f2059]) ).
fof(f2065,plain,
( point_equal(f,b)
| ~ spl3_6 ),
inference(resolution,[],[f185,f76]) ).
fof(f2066,plain,
( spl3_161
| ~ spl3_6 ),
inference(avatar_split_clause,[],[f2065,f183,f1295]) ).
fof(f2071,plain,
( incident(e,p)
| ~ spl3_256 ),
inference(resolution,[],[f1962,f113]) ).
fof(f2077,plain,
( $false
| spl3_108
| ~ spl3_256 ),
inference(forward_subsumption_resolution,[],[f2071,f945]) ).
fof(f2078,plain,
( spl3_108
| ~ spl3_256 ),
inference(avatar_contradiction_clause,[],[f2077]) ).
fof(f2084,definition,
( spl3_262
<=> incident(i,o) ),
introduced(definition,[new_symbols(definition,[spl3_262])],[avatar_definition]) ).
fof(f2085,plain,
( incident(i,o)
| ~ spl3_262 ),
inference(avatar_component_clause,[],[f2084]) ).
fof(f2086,plain,
( ~ incident(i,o)
| spl3_262 ),
inference(avatar_component_clause,[],[f2084]) ).
fof(f2093,definition,
( spl3_264
<=> incident(f,o) ),
introduced(definition,[new_symbols(definition,[spl3_264])],[avatar_definition]) ).
fof(f2094,plain,
( incident(f,o)
| ~ spl3_264 ),
inference(avatar_component_clause,[],[f2093]) ).
fof(f2095,plain,
( ~ incident(f,o)
| spl3_264 ),
inference(avatar_component_clause,[],[f2093]) ).
fof(f2123,plain,
( point_equal(e,b)
| ~ incident(e,l)
| ~ spl3_53 ),
inference(resolution,[],[f560,f108]) ).
fof(f2128,plain,
! [X0] :
( ~ incident(X0,q)
| ~ incident(X0,s)
| line_equal(q,s)
| point_equal(X0,a) ),
inference(resolution,[],[f1753,f133]) ).
fof(f2146,definition,
( spl3_266
<=> ! [X0] :
( ~ incident(X0,q)
| point_equal(X0,a)
| ~ incident(X0,s) ) ),
introduced(definition,[new_symbols(definition,[spl3_266])],[avatar_definition]) ).
fof(f2147,plain,
( ! [X0] :
( ~ incident(X0,s)
| point_equal(X0,a)
| ~ incident(X0,q) )
| ~ spl3_266 ),
inference(avatar_component_clause,[],[f2146]) ).
fof(f2148,plain,
( spl3_238
| spl3_266 ),
inference(avatar_split_clause,[],[f2128,f2146,f1881]) ).
fof(f2315,plain,
incident(i,r),
inference(resolution,[],[f67,f74]) ).
fof(f2316,plain,
incident(d,r),
inference(resolution,[],[f67,f73]) ).
fof(f2317,plain,
incident(c,r),
inference(resolution,[],[f67,f72]) ).
fof(f2319,plain,
( ~ incident(h,r)
| ~ incident(g,r) ),
inference(resolution,[],[f2315,f94]) ).
fof(f2320,plain,
! [X0,X1] :
( ~ incident(i,X0)
| ~ incident(X1,X0)
| ~ incident(X1,r)
| line_equal(X0,r)
| point_equal(X1,i) ),
inference(resolution,[],[f2315,f84]) ).
fof(f2325,definition,
( spl3_301
<=> incident(g,r) ),
introduced(definition,[new_symbols(definition,[spl3_301])],[avatar_definition]) ).
fof(f2326,plain,
( incident(g,r)
| ~ spl3_301 ),
inference(avatar_component_clause,[],[f2325]) ).
fof(f2327,plain,
( ~ incident(g,r)
| spl3_301 ),
inference(avatar_component_clause,[],[f2325]) ).
fof(f2329,definition,
( spl3_302
<=> incident(h,r) ),
introduced(definition,[new_symbols(definition,[spl3_302])],[avatar_definition]) ).
fof(f2330,plain,
( incident(h,r)
| ~ spl3_302 ),
inference(avatar_component_clause,[],[f2329]) ).
fof(f2331,plain,
( ~ incident(h,r)
| spl3_302 ),
inference(avatar_component_clause,[],[f2329]) ).
fof(f2332,plain,
( ~ spl3_301
| ~ spl3_302 ),
inference(avatar_split_clause,[],[f2319,f2329,f2325]) ).
fof(f2338,definition,
( spl3_304
<=> ! [X0] :
( ~ incident(X0,r)
| point_equal(X0,i)
| ~ incident(X0,s) ) ),
introduced(definition,[new_symbols(definition,[spl3_304])],[avatar_definition]) ).
fof(f2339,plain,
( ! [X0] :
( ~ incident(X0,s)
| point_equal(X0,i)
| ~ incident(X0,r) )
| ~ spl3_304 ),
inference(avatar_component_clause,[],[f2338]) ).
fof(f2342,plain,
! [X0] :
( ~ incident(X0,r)
| ~ incident(X0,l)
| line_equal(r,l)
| point_equal(X0,c) ),
inference(resolution,[],[f2317,f145]) ).
fof(f2343,plain,
! [X0,X1] :
( ~ incident(c,X0)
| ~ incident(X1,X0)
| ~ incident(X1,r)
| line_equal(X0,r)
| point_equal(X1,c) ),
inference(resolution,[],[f2317,f84]) ).
fof(f2344,plain,
! [X0] :
( ~ line_equal(r,X0)
| incident(c,X0) ),
inference(resolution,[],[f2317,f82]) ).
fof(f2348,definition,
( spl3_305
<=> line_equal(r,l) ),
introduced(definition,[new_symbols(definition,[spl3_305])],[avatar_definition]) ).
fof(f2350,plain,
( line_equal(r,l)
| ~ spl3_305 ),
inference(avatar_component_clause,[],[f2348]) ).
fof(f2352,definition,
( spl3_306
<=> ! [X0] :
( ~ incident(X0,r)
| point_equal(X0,c)
| ~ incident(X0,l) ) ),
introduced(definition,[new_symbols(definition,[spl3_306])],[avatar_definition]) ).
fof(f2353,plain,
( ! [X0] :
( ~ incident(X0,r)
| point_equal(X0,c)
| ~ incident(X0,l) )
| ~ spl3_306 ),
inference(avatar_component_clause,[],[f2352]) ).
fof(f2354,plain,
( spl3_305
| spl3_306 ),
inference(avatar_split_clause,[],[f2342,f2352,f2348]) ).
fof(f2360,definition,
( spl3_308
<=> ! [X0] :
( ~ incident(X0,r)
| point_equal(X0,c)
| ~ incident(X0,o) ) ),
introduced(definition,[new_symbols(definition,[spl3_308])],[avatar_definition]) ).
fof(f2361,plain,
( ! [X0] :
( ~ incident(X0,r)
| point_equal(X0,c)
| ~ incident(X0,o) )
| ~ spl3_308 ),
inference(avatar_component_clause,[],[f2360]) ).
fof(f2364,plain,
! [X0] :
( ~ incident(X0,r)
| ~ incident(X0,m)
| line_equal(r,m)
| point_equal(X0,d) ),
inference(resolution,[],[f2316,f148]) ).
fof(f2365,plain,
! [X0,X1] :
( ~ incident(d,X0)
| ~ incident(X1,X0)
| ~ incident(X1,r)
| line_equal(X0,r)
| point_equal(X1,d) ),
inference(resolution,[],[f2316,f84]) ).
fof(f2366,plain,
! [X0] :
( ~ line_equal(r,X0)
| incident(d,X0) ),
inference(resolution,[],[f2316,f82]) ).
fof(f2370,definition,
( spl3_309
<=> line_equal(r,m) ),
introduced(definition,[new_symbols(definition,[spl3_309])],[avatar_definition]) ).
fof(f2372,plain,
( line_equal(r,m)
| ~ spl3_309 ),
inference(avatar_component_clause,[],[f2370]) ).
fof(f2374,definition,
( spl3_310
<=> ! [X0] :
( ~ incident(X0,r)
| point_equal(X0,d)
| ~ incident(X0,m) ) ),
introduced(definition,[new_symbols(definition,[spl3_310])],[avatar_definition]) ).
fof(f2375,plain,
( ! [X0] :
( ~ incident(X0,r)
| point_equal(X0,d)
| ~ incident(X0,m) )
| ~ spl3_310 ),
inference(avatar_component_clause,[],[f2374]) ).
fof(f2376,plain,
( spl3_309
| spl3_310 ),
inference(avatar_split_clause,[],[f2364,f2374,f2370]) ).
fof(f2382,definition,
( spl3_312
<=> ! [X0] :
( ~ incident(X0,r)
| point_equal(X0,d)
| ~ incident(X0,p) ) ),
introduced(definition,[new_symbols(definition,[spl3_312])],[avatar_definition]) ).
fof(f2383,plain,
( ! [X0] :
( ~ incident(X0,r)
| point_equal(X0,d)
| ~ incident(X0,p) )
| ~ spl3_312 ),
inference(avatar_component_clause,[],[f2382]) ).
fof(f2387,plain,
( incident(c,m)
| ~ spl3_309 ),
inference(resolution,[],[f2372,f2344]) ).
fof(f2391,plain,
( incident(d,l)
| ~ spl3_305 ),
inference(resolution,[],[f2350,f2366]) ).
fof(f2396,plain,
! [X0] :
( ~ incident(X0,m)
| ~ incident(X0,r)
| line_equal(m,r)
| point_equal(X0,d) ),
inference(resolution,[],[f2365,f109]) ).
fof(f2397,plain,
! [X0] :
( ~ incident(X0,p)
| ~ incident(X0,r)
| line_equal(p,r)
| point_equal(X0,d) ),
inference(resolution,[],[f2365,f509]) ).
fof(f2415,definition,
( spl3_313
<=> line_equal(p,r) ),
introduced(definition,[new_symbols(definition,[spl3_313])],[avatar_definition]) ).
fof(f2417,plain,
( line_equal(p,r)
| ~ spl3_313 ),
inference(avatar_component_clause,[],[f2415]) ).
fof(f2418,plain,
( spl3_313
| spl3_312 ),
inference(avatar_split_clause,[],[f2397,f2382,f2415]) ).
fof(f2475,plain,
! [X0] :
( ~ incident(X0,l)
| ~ incident(X0,r)
| line_equal(l,r)
| point_equal(X0,c) ),
inference(resolution,[],[f2343,f95]) ).
fof(f2476,plain,
! [X0] :
( ~ incident(X0,o)
| ~ incident(X0,r)
| line_equal(o,r)
| point_equal(X0,c) ),
inference(resolution,[],[f2343,f259]) ).
fof(f2494,definition,
( spl3_328
<=> line_equal(o,r) ),
introduced(definition,[new_symbols(definition,[spl3_328])],[avatar_definition]) ).
fof(f2496,plain,
( line_equal(o,r)
| ~ spl3_328 ),
inference(avatar_component_clause,[],[f2494]) ).
fof(f2497,plain,
( spl3_328
| spl3_308 ),
inference(avatar_split_clause,[],[f2476,f2360,f2494]) ).
fof(f2555,plain,
! [X0] :
( ~ incident(X0,s)
| ~ incident(X0,r)
| line_equal(s,r)
| point_equal(X0,i) ),
inference(resolution,[],[f2320,f1503]) ).
fof(f2580,plain,
! [X0] :
( ~ incident(X0,s)
| ~ incident(X0,r)
| point_equal(X0,i) ),
inference(forward_subsumption_resolution,[],[f2555,f91]) ).
fof(f2630,plain,
spl3_304,
inference(avatar_split_clause,[],[f2580,f2338]) ).
fof(f2892,plain,
( incident(b,q)
| ~ spl3_70 ),
inference(resolution,[],[f733,f101]) ).
fof(f2893,plain,
( ! [X0] :
( ~ line_equal(X0,l)
| line_equal(X0,q) )
| ~ spl3_70 ),
inference(resolution,[],[f733,f80]) ).
fof(f2896,plain,
( line_equal(p,q)
| ~ spl3_48
| ~ spl3_70 ),
inference(resolution,[],[f2893,f523]) ).
fof(f2898,plain,
( $false
| ~ spl3_48
| ~ spl3_70 ),
inference(forward_subsumption_resolution,[],[f2896,f92]) ).
fof(f2899,plain,
( ~ spl3_48
| ~ spl3_70 ),
inference(avatar_contradiction_clause,[],[f2898]) ).
fof(f2901,definition,
( spl3_399
<=> incident(d,l) ),
introduced(definition,[new_symbols(definition,[spl3_399])],[avatar_definition]) ).
fof(f2902,plain,
( incident(d,l)
| ~ spl3_399 ),
inference(avatar_component_clause,[],[f2901]) ).
fof(f2903,plain,
( ~ incident(d,l)
| spl3_399 ),
inference(avatar_component_clause,[],[f2901]) ).
fof(f2905,definition,
( spl3_400
<=> point_equal(d,b) ),
introduced(definition,[new_symbols(definition,[spl3_400])],[avatar_definition]) ).
fof(f2907,plain,
( point_equal(d,b)
| ~ spl3_400 ),
inference(avatar_component_clause,[],[f2905]) ).
fof(f2913,plain,
( point_equal(b,h)
| ~ incident(b,p)
| ~ spl3_70
| ~ spl3_77 ),
inference(resolution,[],[f2892,f748]) ).
fof(f2918,plain,
( point_equal(b,h)
| ~ spl3_70
| ~ spl3_77 ),
inference(forward_subsumption_resolution,[],[f2913,f510]) ).
fof(f2922,plain,
( point_equal(h,b)
| ~ spl3_70
| ~ spl3_77 ),
inference(resolution,[],[f2918,f76]) ).
fof(f3405,plain,
( ~ incident(h,sK1(e,i))
| ~ incident(g,sK1(e,i))
| ~ spl3_10 ),
inference(resolution,[],[f1717,f94]) ).
fof(f3411,definition,
( spl3_471
<=> incident(g,sK1(e,i)) ),
introduced(definition,[new_symbols(definition,[spl3_471])],[avatar_definition]) ).
fof(f3413,plain,
( ~ incident(g,sK1(e,i))
| spl3_471 ),
inference(avatar_component_clause,[],[f3411]) ).
fof(f3415,definition,
( spl3_472
<=> incident(h,sK1(e,i)) ),
introduced(definition,[new_symbols(definition,[spl3_472])],[avatar_definition]) ).
fof(f3418,plain,
( ~ spl3_471
| ~ spl3_472
| ~ spl3_10 ),
inference(avatar_split_clause,[],[f3405,f225,f3415,f3411]) ).
fof(f3476,plain,
( point_equal(h,a)
| ~ spl3_107 ),
inference(resolution,[],[f940,f76]) ).
fof(f3511,plain,
( ! [X0] :
( ~ incident(a,X0)
| incident(h,X0) )
| ~ spl3_107 ),
inference(resolution,[],[f3476,f81]) ).
fof(f3514,plain,
( incident(h,l)
| ~ spl3_107 ),
inference(resolution,[],[f3511,f97]) ).
fof(f3518,plain,
( incident(h,s)
| ~ spl3_107 ),
inference(resolution,[],[f3511,f1505]) ).
fof(f3563,definition,
( spl3_481
<=> incident(i,n) ),
introduced(definition,[new_symbols(definition,[spl3_481])],[avatar_definition]) ).
fof(f3564,plain,
( incident(i,n)
| ~ spl3_481 ),
inference(avatar_component_clause,[],[f3563]) ).
fof(f3565,plain,
( ~ incident(i,n)
| spl3_481 ),
inference(avatar_component_clause,[],[f3563]) ).
fof(f3567,definition,
( spl3_482
<=> point_equal(i,f) ),
introduced(definition,[new_symbols(definition,[spl3_482])],[avatar_definition]) ).
fof(f3568,plain,
( ~ point_equal(i,f)
| spl3_482 ),
inference(avatar_component_clause,[],[f3567]) ).
fof(f3569,plain,
( point_equal(i,f)
| ~ spl3_482 ),
inference(avatar_component_clause,[],[f3567]) ).
fof(f3613,definition,
( spl3_485
<=> incident(a,n) ),
introduced(definition,[new_symbols(definition,[spl3_485])],[avatar_definition]) ).
fof(f3614,plain,
( incident(a,n)
| ~ spl3_485 ),
inference(avatar_component_clause,[],[f3613]) ).
fof(f3615,plain,
( ~ incident(a,n)
| spl3_485 ),
inference(avatar_component_clause,[],[f3613]) ).
fof(f3617,definition,
( spl3_486
<=> point_equal(a,f) ),
introduced(definition,[new_symbols(definition,[spl3_486])],[avatar_definition]) ).
fof(f3618,plain,
( ~ point_equal(a,f)
| spl3_486 ),
inference(avatar_component_clause,[],[f3617]) ).
fof(f3619,plain,
( point_equal(a,f)
| ~ spl3_486 ),
inference(avatar_component_clause,[],[f3617]) ).
fof(f3627,plain,
( $false
| spl3_3
| ~ spl3_4 ),
inference(forward_subsumption_resolution,[],[f303,f172]) ).
fof(f3628,plain,
( spl3_3
| ~ spl3_4 ),
inference(avatar_contradiction_clause,[],[f3627]) ).
fof(f3629,plain,
( spl3_188
| ~ spl3_4 ),
inference(avatar_split_clause,[],[f1722,f174,f1514]) ).
fof(f3643,plain,
( point_equal(a,b)
| ~ incident(a,l)
| ~ spl3_53
| ~ spl3_260 ),
inference(resolution,[],[f2056,f560]) ).
fof(f3648,plain,
( point_equal(a,b)
| ~ spl3_53
| ~ spl3_260 ),
inference(forward_subsumption_resolution,[],[f3643,f97]) ).
fof(f3677,definition,
( spl3_489
<=> line_equal(m,o) ),
introduced(definition,[new_symbols(definition,[spl3_489])],[avatar_definition]) ).
fof(f3678,plain,
( ~ line_equal(m,o)
| spl3_489 ),
inference(avatar_component_clause,[],[f3677]) ).
fof(f3679,plain,
( line_equal(m,o)
| ~ spl3_489 ),
inference(avatar_component_clause,[],[f3677]) ).
fof(f3684,plain,
( ! [X0] :
( ~ incident(e,X0)
| incident(a,X0) )
| ~ spl3_261 ),
inference(resolution,[],[f2061,f81]) ).
fof(f3686,plain,
( point_equal(e,a)
| ~ spl3_261 ),
inference(resolution,[],[f2061,f76]) ).
fof(f3713,plain,
( incident(a,m)
| ~ spl3_261 ),
inference(resolution,[],[f3684,f108]) ).
fof(f3782,plain,
( ! [X0] :
( ~ incident(f,X0)
| incident(a,X0) )
| ~ spl3_486 ),
inference(resolution,[],[f3619,f81]) ).
fof(f3803,plain,
( point_equal(a,b)
| ~ incident(a,l)
| ~ spl3_28
| ~ spl3_485 ),
inference(resolution,[],[f3614,f387]) ).
fof(f3813,plain,
( ! [X0] :
( ~ incident(a,X0)
| incident(e,X0) )
| ~ spl3_261 ),
inference(resolution,[],[f3686,f81]) ).
fof(f3816,plain,
( incident(e,l)
| ~ spl3_261 ),
inference(resolution,[],[f3813,f97]) ).
fof(f3818,plain,
( incident(e,n)
| ~ spl3_261
| ~ spl3_485 ),
inference(resolution,[],[f3813,f3614]) ).
fof(f3839,plain,
( $false
| spl3_69
| ~ spl3_261
| ~ spl3_485 ),
inference(forward_subsumption_resolution,[],[f3818,f678]) ).
fof(f3840,plain,
( spl3_69
| ~ spl3_261
| ~ spl3_485 ),
inference(avatar_contradiction_clause,[],[f3839]) ).
fof(f3853,plain,
( spl3_6
| ~ spl3_2
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f2047,f179,f163,f183]) ).
fof(f3862,plain,
( ! [X0] :
( ~ incident(b,X0)
| incident(f,X0) )
| ~ spl3_161 ),
inference(resolution,[],[f1297,f81]) ).
fof(f3864,plain,
( point_equal(b,f)
| ~ spl3_161 ),
inference(resolution,[],[f1297,f76]) ).
fof(f3865,plain,
( ! [X0] :
( ~ incident(f,X0)
| incident(b,X0) )
| ~ spl3_6 ),
inference(resolution,[],[f185,f81]) ).
fof(f3868,plain,
( incident(f,l)
| ~ spl3_161 ),
inference(resolution,[],[f3862,f96]) ).
fof(f3872,plain,
( incident(f,p)
| ~ spl3_161 ),
inference(resolution,[],[f3862,f510]) ).
fof(f3891,plain,
( $false
| spl3_160
| ~ spl3_161 ),
inference(forward_subsumption_resolution,[],[f3868,f1293]) ).
fof(f3892,plain,
( spl3_160
| ~ spl3_161 ),
inference(avatar_contradiction_clause,[],[f3891]) ).
fof(f3895,plain,
( ! [X0] :
( ~ incident(X0,l)
| ~ incident(X0,s)
| line_equal(l,s)
| point_equal(X0,f) )
| ~ spl3_160 ),
inference(resolution,[],[f1292,f1724]) ).
fof(f3910,definition,
( spl3_496
<=> line_equal(l,s) ),
introduced(definition,[new_symbols(definition,[spl3_496])],[avatar_definition]) ).
fof(f3912,plain,
( line_equal(l,s)
| ~ spl3_496 ),
inference(avatar_component_clause,[],[f3910]) ).
fof(f3914,definition,
( spl3_497
<=> ! [X0] :
( ~ incident(X0,l)
| point_equal(X0,f)
| ~ incident(X0,s) ) ),
introduced(definition,[new_symbols(definition,[spl3_497])],[avatar_definition]) ).
fof(f3915,plain,
( ! [X0] :
( ~ incident(X0,s)
| point_equal(X0,f)
| ~ incident(X0,l) )
| ~ spl3_497 ),
inference(avatar_component_clause,[],[f3914]) ).
fof(f3916,plain,
( spl3_496
| spl3_497
| ~ spl3_160 ),
inference(avatar_split_clause,[],[f3895,f1291,f3914,f3910]) ).
fof(f3920,definition,
( spl3_498
<=> incident(f,p) ),
introduced(definition,[new_symbols(definition,[spl3_498])],[avatar_definition]) ).
fof(f3921,plain,
( incident(f,p)
| ~ spl3_498 ),
inference(avatar_component_clause,[],[f3920]) ).
fof(f3924,definition,
( spl3_499
<=> point_equal(f,h) ),
introduced(definition,[new_symbols(definition,[spl3_499])],[avatar_definition]) ).
fof(f3925,plain,
( ~ point_equal(f,h)
| spl3_499 ),
inference(avatar_component_clause,[],[f3924]) ).
fof(f3926,plain,
( point_equal(f,h)
| ~ spl3_499 ),
inference(avatar_component_clause,[],[f3924]) ).
fof(f3928,plain,
( spl3_498
| ~ spl3_161 ),
inference(avatar_split_clause,[],[f3872,f1295,f3920]) ).
fof(f3930,plain,
( incident(b,m)
| ~ spl3_6 ),
inference(resolution,[],[f3865,f107]) ).
fof(f4012,plain,
( ! [X0] :
( ~ incident(b,X0)
| incident(a,X0) )
| ~ spl3_53
| ~ spl3_260 ),
inference(resolution,[],[f3648,f81]) ).
fof(f4019,plain,
( incident(a,p)
| ~ spl3_53
| ~ spl3_260 ),
inference(resolution,[],[f4012,f510]) ).
fof(f4038,plain,
( $false
| ~ spl3_53
| spl3_106
| ~ spl3_260 ),
inference(forward_subsumption_resolution,[],[f4019,f936]) ).
fof(f4039,plain,
( ~ spl3_53
| spl3_106
| ~ spl3_260 ),
inference(avatar_contradiction_clause,[],[f4038]) ).
fof(f4040,plain,
( $false
| ~ spl3_52
| spl3_399 ),
inference(forward_subsumption_resolution,[],[f1985,f2903]) ).
fof(f4041,plain,
( ~ spl3_52
| spl3_399 ),
inference(avatar_contradiction_clause,[],[f4040]) ).
fof(f4044,plain,
( point_equal(a,b)
| ~ spl3_28
| ~ spl3_485 ),
inference(forward_subsumption_resolution,[],[f3803,f97]) ).
fof(f4053,definition,
( spl3_502
<=> line_equal(l,p) ),
introduced(definition,[new_symbols(definition,[spl3_502])],[avatar_definition]) ).
fof(f4055,plain,
( line_equal(l,p)
| ~ spl3_502 ),
inference(avatar_component_clause,[],[f4053]) ).
fof(f4061,definition,
( spl3_504
<=> line_equal(l,r) ),
introduced(definition,[new_symbols(definition,[spl3_504])],[avatar_definition]) ).
fof(f4063,plain,
( line_equal(l,r)
| ~ spl3_504 ),
inference(avatar_component_clause,[],[f4061]) ).
fof(f4068,plain,
( ! [X0] :
( ~ incident(b,X0)
| incident(a,X0) )
| ~ spl3_28
| ~ spl3_485 ),
inference(resolution,[],[f4044,f81]) ).
fof(f4075,plain,
( incident(a,p)
| ~ spl3_28
| ~ spl3_485 ),
inference(resolution,[],[f4068,f510]) ).
fof(f4094,plain,
( $false
| ~ spl3_28
| spl3_106
| ~ spl3_485 ),
inference(forward_subsumption_resolution,[],[f4075,f936]) ).
fof(f4095,plain,
( ~ spl3_28
| spl3_106
| ~ spl3_485 ),
inference(avatar_contradiction_clause,[],[f4094]) ).
fof(f4098,definition,
( spl3_506
<=> incident(g,l) ),
introduced(definition,[new_symbols(definition,[spl3_506])],[avatar_definition]) ).
fof(f4099,plain,
( incident(g,l)
| ~ spl3_506 ),
inference(avatar_component_clause,[],[f4098]) ).
fof(f4102,definition,
( spl3_507
<=> point_equal(g,c) ),
introduced(definition,[new_symbols(definition,[spl3_507])],[avatar_definition]) ).
fof(f4104,plain,
( point_equal(g,c)
| ~ spl3_507 ),
inference(avatar_component_clause,[],[f4102]) ).
fof(f4107,definition,
( spl3_508
<=> point_equal(g,b) ),
introduced(definition,[new_symbols(definition,[spl3_508])],[avatar_definition]) ).
fof(f4108,plain,
( ~ point_equal(g,b)
| spl3_508 ),
inference(avatar_component_clause,[],[f4107]) ).
fof(f4109,plain,
( point_equal(g,b)
| ~ spl3_508 ),
inference(avatar_component_clause,[],[f4107]) ).
fof(f4211,plain,
( spl3_4
| ~ spl3_2
| ~ spl3_3 ),
inference(avatar_split_clause,[],[f299,f170,f163,f174]) ).
fof(f4245,plain,
( ! [X0] :
( ~ incident(b,X0)
| incident(g,X0) )
| ~ spl3_508 ),
inference(resolution,[],[f4109,f81]) ).
fof(f4248,plain,
( incident(a,m)
| ~ spl3_486 ),
inference(resolution,[],[f3782,f107]) ).
fof(f4249,plain,
( incident(a,n)
| ~ spl3_486 ),
inference(resolution,[],[f3782,f120]) ).
fof(f4270,plain,
( $false
| spl3_485
| ~ spl3_486 ),
inference(forward_subsumption_resolution,[],[f4249,f3615]) ).
fof(f4271,plain,
( spl3_485
| ~ spl3_486 ),
inference(avatar_contradiction_clause,[],[f4270]) ).
fof(f4299,plain,
( incident(g,p)
| ~ spl3_508 ),
inference(resolution,[],[f4245,f510]) ).
fof(f4365,plain,
( incident(d,o)
| ~ spl3_489 ),
inference(resolution,[],[f3679,f116]) ).
fof(f4373,plain,
( point_equal(d,b)
| ~ incident(d,n)
| ~ spl3_59 ),
inference(resolution,[],[f614,f509]) ).
fof(f4378,definition,
( spl3_516
<=> incident(d,n) ),
introduced(definition,[new_symbols(definition,[spl3_516])],[avatar_definition]) ).
fof(f4379,plain,
( incident(d,n)
| ~ spl3_516 ),
inference(avatar_component_clause,[],[f4378]) ).
fof(f4380,plain,
( ~ incident(d,n)
| spl3_516 ),
inference(avatar_component_clause,[],[f4378]) ).
fof(f4381,plain,
( ~ spl3_516
| spl3_400
| ~ spl3_59 ),
inference(avatar_split_clause,[],[f4373,f613,f2905,f4378]) ).
fof(f4398,definition,
( spl3_519
<=> incident(h,o) ),
introduced(definition,[new_symbols(definition,[spl3_519])],[avatar_definition]) ).
fof(f4399,plain,
( incident(h,o)
| ~ spl3_519 ),
inference(avatar_component_clause,[],[f4398]) ).
fof(f4403,definition,
( spl3_520
<=> incident(b,o) ),
introduced(definition,[new_symbols(definition,[spl3_520])],[avatar_definition]) ).
fof(f4404,plain,
( incident(b,o)
| ~ spl3_520 ),
inference(avatar_component_clause,[],[f4403]) ).
fof(f4405,plain,
( ~ incident(b,o)
| spl3_520 ),
inference(avatar_component_clause,[],[f4403]) ).
fof(f4407,definition,
( spl3_521
<=> point_equal(b,e) ),
introduced(definition,[new_symbols(definition,[spl3_521])],[avatar_definition]) ).
fof(f4409,plain,
( point_equal(b,e)
| ~ spl3_521 ),
inference(avatar_component_clause,[],[f4407]) ).
fof(f4462,plain,
( point_equal(h,f)
| ~ spl3_499 ),
inference(resolution,[],[f3926,f76]) ).
fof(f4475,definition,
( spl3_523
<=> incident(c,p) ),
introduced(definition,[new_symbols(definition,[spl3_523])],[avatar_definition]) ).
fof(f4476,plain,
( incident(c,p)
| ~ spl3_523 ),
inference(avatar_component_clause,[],[f4475]) ).
fof(f4477,plain,
( ~ incident(c,p)
| spl3_523 ),
inference(avatar_component_clause,[],[f4475]) ).
fof(f4546,plain,
( ~ incident(h,sK1(b,i))
| ~ incident(g,sK1(b,i))
| ~ spl3_10 ),
inference(resolution,[],[f1716,f94]) ).
fof(f4552,definition,
( spl3_531
<=> incident(g,sK1(b,i)) ),
introduced(definition,[new_symbols(definition,[spl3_531])],[avatar_definition]) ).
fof(f4554,plain,
( ~ incident(g,sK1(b,i))
| spl3_531 ),
inference(avatar_component_clause,[],[f4552]) ).
fof(f4556,definition,
( spl3_532
<=> incident(h,sK1(b,i)) ),
introduced(definition,[new_symbols(definition,[spl3_532])],[avatar_definition]) ).
fof(f4558,plain,
( ~ incident(h,sK1(b,i))
| spl3_532 ),
inference(avatar_component_clause,[],[f4556]) ).
fof(f4559,plain,
( ~ spl3_531
| ~ spl3_532
| ~ spl3_10 ),
inference(avatar_split_clause,[],[f4546,f225,f4556,f4552]) ).
fof(f4590,plain,
( ! [X0] :
( ~ incident(X0,o)
| ~ incident(X0,n)
| line_equal(o,n)
| point_equal(X0,f) )
| ~ spl3_264 ),
inference(resolution,[],[f149,f2094]) ).
fof(f4621,definition,
( spl3_539
<=> line_equal(o,n) ),
introduced(definition,[new_symbols(definition,[spl3_539])],[avatar_definition]) ).
fof(f4623,plain,
( line_equal(o,n)
| ~ spl3_539 ),
inference(avatar_component_clause,[],[f4621]) ).
fof(f4625,definition,
( spl3_540
<=> ! [X0] :
( ~ incident(X0,o)
| point_equal(X0,f)
| ~ incident(X0,n) ) ),
introduced(definition,[new_symbols(definition,[spl3_540])],[avatar_definition]) ).
fof(f4626,plain,
( ! [X0] :
( ~ incident(X0,o)
| point_equal(X0,f)
| ~ incident(X0,n) )
| ~ spl3_540 ),
inference(avatar_component_clause,[],[f4625]) ).
fof(f4627,plain,
( spl3_539
| spl3_540
| ~ spl3_264 ),
inference(avatar_split_clause,[],[f4590,f2093,f4625,f4621]) ).
fof(f4705,plain,
( line_equal(n,o)
| ~ spl3_539 ),
inference(resolution,[],[f4623,f79]) ).
fof(f4706,plain,
( $false
| ~ spl3_539 ),
inference(forward_subsumption_resolution,[],[f4705,f93]) ).
fof(f4707,plain,
~ spl3_539,
inference(avatar_contradiction_clause,[],[f4706]) ).
fof(f4838,plain,
( point_equal(c,e)
| ~ incident(c,m)
| ~ spl3_18 ),
inference(resolution,[],[f271,f259]) ).
fof(f4840,plain,
( point_equal(f,e)
| ~ incident(f,m)
| ~ spl3_18
| ~ spl3_264 ),
inference(resolution,[],[f271,f2094]) ).
fof(f4845,plain,
( point_equal(f,e)
| ~ spl3_18
| ~ spl3_264 ),
inference(forward_subsumption_resolution,[],[f4840,f107]) ).
fof(f4847,plain,
( ! [X0] :
( ~ incident(e,X0)
| incident(f,X0) )
| ~ spl3_18
| ~ spl3_264 ),
inference(resolution,[],[f4845,f81]) ).
fof(f4852,plain,
( incident(f,q)
| ~ spl3_18
| ~ spl3_264 ),
inference(resolution,[],[f4847,f132]) ).
fof(f4877,plain,
( ! [X0] :
( ~ incident(X0,m)
| ~ incident(X0,o)
| point_equal(X0,e) )
| spl3_489 ),
inference(forward_subsumption_resolution,[],[f318,f3678]) ).
fof(f4878,plain,
( spl3_18
| spl3_489 ),
inference(avatar_split_clause,[],[f4877,f3677,f270]) ).
fof(f4920,plain,
( ! [X0] :
( ~ incident(X0,m)
| ~ incident(X0,n)
| line_equal(m,n)
| point_equal(X0,g) )
| ~ spl3_3 ),
inference(resolution,[],[f151,f171]) ).
fof(f4964,definition,
( spl3_589
<=> line_equal(m,n) ),
introduced(definition,[new_symbols(definition,[spl3_589])],[avatar_definition]) ).
fof(f4966,plain,
( line_equal(m,n)
| ~ spl3_589 ),
inference(avatar_component_clause,[],[f4964]) ).
fof(f4968,definition,
( spl3_590
<=> ! [X0] :
( ~ incident(X0,m)
| point_equal(X0,g)
| ~ incident(X0,n) ) ),
introduced(definition,[new_symbols(definition,[spl3_590])],[avatar_definition]) ).
fof(f4969,plain,
( ! [X0] :
( ~ incident(X0,n)
| point_equal(X0,g)
| ~ incident(X0,m) )
| ~ spl3_590 ),
inference(avatar_component_clause,[],[f4968]) ).
fof(f4970,plain,
( spl3_589
| spl3_590
| ~ spl3_3 ),
inference(avatar_split_clause,[],[f4920,f170,f4968,f4964]) ).
fof(f5048,plain,
( line_equal(n,m)
| ~ spl3_589 ),
inference(resolution,[],[f4966,f79]) ).
fof(f5049,plain,
( $false
| spl3_1
| ~ spl3_589 ),
inference(forward_subsumption_resolution,[],[f5048,f160]) ).
fof(f5050,plain,
( spl3_1
| ~ spl3_589 ),
inference(avatar_contradiction_clause,[],[f5049]) ).
fof(f5072,plain,
( point_equal(d,c)
| ~ incident(d,o)
| ~ spl3_308 ),
inference(resolution,[],[f2361,f2316]) ).
fof(f5078,plain,
( point_equal(d,c)
| ~ spl3_308
| ~ spl3_489 ),
inference(forward_subsumption_resolution,[],[f5072,f4365]) ).
fof(f5090,plain,
( ! [X0] :
( ~ incident(c,X0)
| incident(d,X0) )
| ~ spl3_308
| ~ spl3_489 ),
inference(resolution,[],[f5078,f81]) ).
fof(f5093,plain,
( incident(d,l)
| ~ spl3_308
| ~ spl3_489 ),
inference(resolution,[],[f5090,f95]) ).
fof(f5116,plain,
( point_equal(d,b)
| ~ incident(d,l)
| ~ spl3_49 ),
inference(resolution,[],[f526,f509]) ).
fof(f5120,plain,
( point_equal(d,b)
| ~ spl3_49
| ~ spl3_399 ),
inference(forward_subsumption_resolution,[],[f5116,f2902]) ).
fof(f5126,plain,
( spl3_400
| ~ spl3_49
| ~ spl3_399 ),
inference(avatar_split_clause,[],[f5120,f2901,f525,f2905]) ).
fof(f5127,plain,
( ! [X0] :
( ~ incident(b,X0)
| incident(d,X0) )
| ~ spl3_400 ),
inference(resolution,[],[f2907,f81]) ).
fof(f5131,plain,
( incident(d,n)
| ~ spl3_400 ),
inference(resolution,[],[f5127,f121]) ).
fof(f5152,plain,
( $false
| ~ spl3_400
| spl3_516 ),
inference(forward_subsumption_resolution,[],[f5131,f4380]) ).
fof(f5153,plain,
( ~ spl3_400
| spl3_516 ),
inference(avatar_contradiction_clause,[],[f5152]) ).
fof(f5157,plain,
( point_equal(d,g)
| ~ incident(d,m)
| ~ spl3_516
| ~ spl3_590 ),
inference(resolution,[],[f4379,f4969]) ).
fof(f5158,plain,
( point_equal(d,f)
| ~ incident(d,m)
| ~ spl3_2
| ~ spl3_516 ),
inference(resolution,[],[f4379,f164]) ).
fof(f5164,plain,
( point_equal(d,f)
| ~ spl3_2
| ~ spl3_516 ),
inference(forward_subsumption_resolution,[],[f5158,f109]) ).
fof(f5165,plain,
( point_equal(d,g)
| ~ spl3_516
| ~ spl3_590 ),
inference(forward_subsumption_resolution,[],[f5157,f109]) ).
fof(f5172,plain,
( point_equal(f,d)
| ~ spl3_2
| ~ spl3_516 ),
inference(resolution,[],[f5164,f76]) ).
fof(f5198,plain,
( point_equal(g,d)
| ~ spl3_516
| ~ spl3_590 ),
inference(resolution,[],[f5165,f76]) ).
fof(f5223,plain,
( ! [X0] :
( ~ incident(d,X0)
| incident(f,X0) )
| ~ spl3_2
| ~ spl3_516 ),
inference(resolution,[],[f5172,f81]) ).
fof(f5226,plain,
( incident(f,l)
| ~ spl3_2
| ~ spl3_399
| ~ spl3_516 ),
inference(resolution,[],[f5223,f2902]) ).
fof(f5230,plain,
( incident(f,r)
| ~ spl3_2
| ~ spl3_516 ),
inference(resolution,[],[f5223,f2316]) ).
fof(f5251,plain,
( $false
| ~ spl3_2
| spl3_160
| ~ spl3_399
| ~ spl3_516 ),
inference(forward_subsumption_resolution,[],[f5226,f1293]) ).
fof(f5252,plain,
( ~ spl3_2
| spl3_160
| ~ spl3_399
| ~ spl3_516 ),
inference(avatar_contradiction_clause,[],[f5251]) ).
fof(f5257,plain,
( $false
| spl3_6
| ~ spl3_161 ),
inference(forward_subsumption_resolution,[],[f3864,f184]) ).
fof(f5258,plain,
( spl3_6
| ~ spl3_161 ),
inference(avatar_contradiction_clause,[],[f5257]) ).
fof(f5260,plain,
( spl3_516
| ~ spl3_400 ),
inference(avatar_split_clause,[],[f5131,f2905,f4378]) ).
fof(f5262,definition,
( spl3_612
<=> incident(e,l) ),
introduced(definition,[new_symbols(definition,[spl3_612])],[avatar_definition]) ).
fof(f5263,plain,
( incident(e,l)
| ~ spl3_612 ),
inference(avatar_component_clause,[],[f5262]) ).
fof(f5264,plain,
( ~ incident(e,l)
| spl3_612 ),
inference(avatar_component_clause,[],[f5262]) ).
fof(f5272,definition,
( spl3_614
<=> point_equal(e,c) ),
introduced(definition,[new_symbols(definition,[spl3_614])],[avatar_definition]) ).
fof(f5273,plain,
( ~ point_equal(e,c)
| spl3_614 ),
inference(avatar_component_clause,[],[f5272]) ).
fof(f5274,plain,
( point_equal(e,c)
| ~ spl3_614 ),
inference(avatar_component_clause,[],[f5272]) ).
fof(f5278,definition,
( spl3_615
<=> incident(h,n) ),
introduced(definition,[new_symbols(definition,[spl3_615])],[avatar_definition]) ).
fof(f5279,plain,
( incident(h,n)
| ~ spl3_615 ),
inference(avatar_component_clause,[],[f5278]) ).
fof(f5280,plain,
( ~ incident(h,n)
| spl3_615 ),
inference(avatar_component_clause,[],[f5278]) ).
fof(f5282,definition,
( spl3_616
<=> point_equal(h,b) ),
introduced(definition,[new_symbols(definition,[spl3_616])],[avatar_definition]) ).
fof(f5284,plain,
( point_equal(h,b)
| ~ spl3_616 ),
inference(avatar_component_clause,[],[f5282]) ).
fof(f5287,definition,
( spl3_617
<=> incident(h,l) ),
introduced(definition,[new_symbols(definition,[spl3_617])],[avatar_definition]) ).
fof(f5288,plain,
( incident(h,l)
| ~ spl3_617 ),
inference(avatar_component_clause,[],[f5287]) ).
fof(f5289,plain,
( ~ incident(h,l)
| spl3_617 ),
inference(avatar_component_clause,[],[f5287]) ).
fof(f5291,plain,
( $false
| spl3_5
| ~ spl3_6 ),
inference(forward_subsumption_resolution,[],[f3930,f181]) ).
fof(f5292,plain,
( spl3_5
| ~ spl3_6 ),
inference(avatar_contradiction_clause,[],[f5291]) ).
fof(f5341,plain,
( ! [X0] :
( ~ line_equal(m,X0)
| incident(b,X0) )
| ~ spl3_5 ),
inference(resolution,[],[f180,f82]) ).
fof(f5345,plain,
( ! [X0] :
( ~ incident(X0,l)
| ~ incident(X0,n)
| line_equal(l,n)
| point_equal(X0,f) )
| ~ spl3_160 ),
inference(resolution,[],[f1292,f149]) ).
fof(f5354,definition,
( spl3_618
<=> line_equal(l,n) ),
introduced(definition,[new_symbols(definition,[spl3_618])],[avatar_definition]) ).
fof(f5356,plain,
( line_equal(l,n)
| ~ spl3_618 ),
inference(avatar_component_clause,[],[f5354]) ).
fof(f5358,definition,
( spl3_619
<=> ! [X0] :
( ~ incident(X0,l)
| point_equal(X0,f)
| ~ incident(X0,n) ) ),
introduced(definition,[new_symbols(definition,[spl3_619])],[avatar_definition]) ).
fof(f5359,plain,
( ! [X0] :
( ~ incident(X0,n)
| point_equal(X0,f)
| ~ incident(X0,l) )
| ~ spl3_619 ),
inference(avatar_component_clause,[],[f5358]) ).
fof(f5360,plain,
( spl3_618
| spl3_619
| ~ spl3_160 ),
inference(avatar_split_clause,[],[f5345,f1291,f5358,f5354]) ).
fof(f5366,plain,
( ! [X0] :
( ~ line_equal(l,X0)
| incident(g,X0) )
| ~ spl3_506 ),
inference(resolution,[],[f4099,f82]) ).
fof(f5417,plain,
( ! [X0] :
( ~ incident(b,X0)
| incident(f,X0) )
| ~ spl3_161 ),
inference(resolution,[],[f1297,f81]) ).
fof(f5418,plain,
( ! [X0] :
( ~ point_equal(X0,f)
| point_equal(X0,b) )
| ~ spl3_161 ),
inference(resolution,[],[f1297,f77]) ).
fof(f5423,plain,
( ! [X0] :
( ~ incident(c,X0)
| incident(g,X0) )
| ~ spl3_507 ),
inference(resolution,[],[f4104,f81]) ).
fof(f5588,plain,
( incident(g,r)
| ~ spl3_507 ),
inference(resolution,[],[f5423,f2317]) ).
fof(f5610,plain,
( $false
| spl3_301
| ~ spl3_507 ),
inference(forward_subsumption_resolution,[],[f5588,f2327]) ).
fof(f5611,plain,
( spl3_301
| ~ spl3_507 ),
inference(avatar_contradiction_clause,[],[f5610]) ).
fof(f5673,plain,
( ! [X0] :
( ~ incident(b,X0)
| incident(d,X0) )
| ~ spl3_400 ),
inference(resolution,[],[f2907,f81]) ).
fof(f5723,plain,
( point_equal(e,a)
| ~ incident(e,l)
| ~ spl3_71 ),
inference(resolution,[],[f711,f132]) ).
fof(f5724,plain,
( point_equal(h,a)
| ~ incident(h,l)
| ~ spl3_71 ),
inference(resolution,[],[f711,f131]) ).
fof(f5756,plain,
( incident(b,o)
| ~ spl3_5
| ~ spl3_489 ),
inference(resolution,[],[f5341,f3679]) ).
fof(f5782,plain,
( incident(f,o)
| ~ spl3_161
| ~ spl3_520 ),
inference(resolution,[],[f4404,f5417]) ).
fof(f5788,plain,
( ~ incident(b,n)
| point_equal(b,g)
| ~ spl3_520 ),
inference(resolution,[],[f4404,f650]) ).
fof(f5799,plain,
( point_equal(h,e)
| ~ spl3_109 ),
inference(resolution,[],[f949,f76]) ).
fof(f5800,plain,
( spl3_259
| ~ spl3_109 ),
inference(avatar_split_clause,[],[f5799,f947,f2001]) ).
fof(f5968,plain,
( incident(d,l)
| ~ spl3_400 ),
inference(resolution,[],[f5673,f96]) ).
fof(f6211,plain,
( point_equal(c,d)
| ~ incident(c,p)
| ~ spl3_312 ),
inference(resolution,[],[f2383,f2317]) ).
fof(f6218,definition,
( spl3_672
<=> incident(i,p) ),
introduced(definition,[new_symbols(definition,[spl3_672])],[avatar_definition]) ).
fof(f6219,plain,
( incident(i,p)
| ~ spl3_672 ),
inference(avatar_component_clause,[],[f6218]) ).
fof(f6220,plain,
( ~ incident(i,p)
| spl3_672 ),
inference(avatar_component_clause,[],[f6218]) ).
fof(f6222,definition,
( spl3_673
<=> point_equal(i,d) ),
introduced(definition,[new_symbols(definition,[spl3_673])],[avatar_definition]) ).
fof(f6224,plain,
( point_equal(i,d)
| ~ spl3_673 ),
inference(avatar_component_clause,[],[f6222]) ).
fof(f6262,plain,
! [X0] :
( ~ incident(X0,m)
| ~ incident(X0,q)
| line_equal(m,q)
| point_equal(X0,e) ),
inference(resolution,[],[f152,f108]) ).
fof(f6369,plain,
( point_equal(h,d)
| ~ incident(h,m)
| ~ spl3_51 ),
inference(resolution,[],[f539,f508]) ).
fof(f6574,plain,
( point_equal(c,e)
| ~ spl3_614 ),
inference(resolution,[],[f5274,f76]) ).
fof(f6578,plain,
( point_equal(f,a)
| ~ incident(f,q)
| ~ spl3_266 ),
inference(resolution,[],[f2147,f1504]) ).
fof(f6584,definition,
( spl3_721
<=> incident(i,q) ),
introduced(definition,[new_symbols(definition,[spl3_721])],[avatar_definition]) ).
fof(f6585,plain,
( incident(i,q)
| ~ spl3_721 ),
inference(avatar_component_clause,[],[f6584]) ).
fof(f6586,plain,
( ~ incident(i,q)
| spl3_721 ),
inference(avatar_component_clause,[],[f6584]) ).
fof(f6588,definition,
( spl3_722
<=> point_equal(i,a) ),
introduced(definition,[new_symbols(definition,[spl3_722])],[avatar_definition]) ).
fof(f6589,plain,
( ~ point_equal(i,a)
| spl3_722 ),
inference(avatar_component_clause,[],[f6588]) ).
fof(f6590,plain,
( point_equal(i,a)
| ~ spl3_722 ),
inference(avatar_component_clause,[],[f6588]) ).
fof(f6593,definition,
( spl3_723
<=> incident(g,q) ),
introduced(definition,[new_symbols(definition,[spl3_723])],[avatar_definition]) ).
fof(f6594,plain,
( incident(g,q)
| ~ spl3_723 ),
inference(avatar_component_clause,[],[f6593]) ).
fof(f6602,definition,
( spl3_725
<=> incident(f,q) ),
introduced(definition,[new_symbols(definition,[spl3_725])],[avatar_definition]) ).
fof(f6603,plain,
( incident(f,q)
| ~ spl3_725 ),
inference(avatar_component_clause,[],[f6602]) ).
fof(f6604,plain,
( ~ incident(f,q)
| spl3_725 ),
inference(avatar_component_clause,[],[f6602]) ).
fof(f6606,definition,
( spl3_726
<=> point_equal(f,a) ),
introduced(definition,[new_symbols(definition,[spl3_726])],[avatar_definition]) ).
fof(f6607,plain,
( ~ point_equal(f,a)
| spl3_726 ),
inference(avatar_component_clause,[],[f6606]) ).
fof(f6608,plain,
( point_equal(f,a)
| ~ spl3_726 ),
inference(avatar_component_clause,[],[f6606]) ).
fof(f6611,definition,
( spl3_727
<=> incident(c,q) ),
introduced(definition,[new_symbols(definition,[spl3_727])],[avatar_definition]) ).
fof(f6612,plain,
( incident(c,q)
| ~ spl3_727 ),
inference(avatar_component_clause,[],[f6611]) ).
fof(f6615,definition,
( spl3_728
<=> point_equal(c,a) ),
introduced(definition,[new_symbols(definition,[spl3_728])],[avatar_definition]) ).
fof(f6617,plain,
( point_equal(c,a)
| ~ spl3_728 ),
inference(avatar_component_clause,[],[f6615]) ).
fof(f6768,plain,
( point_equal(d,c)
| ~ incident(d,l)
| ~ spl3_306 ),
inference(resolution,[],[f2353,f2316]) ).
fof(f6770,plain,
( point_equal(i,c)
| ~ incident(i,l)
| ~ spl3_306 ),
inference(resolution,[],[f2353,f2315]) ).
fof(f6774,definition,
( spl3_757
<=> incident(i,l) ),
introduced(definition,[new_symbols(definition,[spl3_757])],[avatar_definition]) ).
fof(f6775,plain,
( incident(i,l)
| ~ spl3_757 ),
inference(avatar_component_clause,[],[f6774]) ).
fof(f6776,plain,
( ~ incident(i,l)
| spl3_757 ),
inference(avatar_component_clause,[],[f6774]) ).
fof(f6778,definition,
( spl3_758
<=> point_equal(i,c) ),
introduced(definition,[new_symbols(definition,[spl3_758])],[avatar_definition]) ).
fof(f6779,plain,
( ~ point_equal(i,c)
| spl3_758 ),
inference(avatar_component_clause,[],[f6778]) ).
fof(f6780,plain,
( point_equal(i,c)
| ~ spl3_758 ),
inference(avatar_component_clause,[],[f6778]) ).
fof(f6795,plain,
( point_equal(d,b)
| ~ incident(d,m)
| ~ spl3_257 ),
inference(resolution,[],[f1965,f509]) ).
fof(f6822,plain,
( point_equal(a,f)
| ~ incident(a,m)
| ~ spl3_225 ),
inference(resolution,[],[f1734,f1505]) ).
fof(f6844,definition,
( spl3_760
<=> incident(c,m) ),
introduced(definition,[new_symbols(definition,[spl3_760])],[avatar_definition]) ).
fof(f6845,plain,
( incident(c,m)
| ~ spl3_760 ),
inference(avatar_component_clause,[],[f6844]) ).
fof(f6846,plain,
( ~ incident(c,m)
| spl3_760 ),
inference(avatar_component_clause,[],[f6844]) ).
fof(f6853,definition,
( spl3_762
<=> incident(i,m) ),
introduced(definition,[new_symbols(definition,[spl3_762])],[avatar_definition]) ).
fof(f6854,plain,
( incident(i,m)
| ~ spl3_762 ),
inference(avatar_component_clause,[],[f6853]) ).
fof(f6869,plain,
( ! [X0] :
( ~ incident(X0,m)
| ~ incident(X0,r)
| line_equal(m,r)
| point_equal(X0,c) )
| ~ spl3_760 ),
inference(resolution,[],[f6845,f2343]) ).
fof(f6881,definition,
( spl3_763
<=> line_equal(m,r) ),
introduced(definition,[new_symbols(definition,[spl3_763])],[avatar_definition]) ).
fof(f6882,plain,
( ~ line_equal(m,r)
| spl3_763 ),
inference(avatar_component_clause,[],[f6881]) ).
fof(f6883,plain,
( line_equal(m,r)
| ~ spl3_763 ),
inference(avatar_component_clause,[],[f6881]) ).
fof(f6885,definition,
( spl3_764
<=> ! [X0] :
( ~ incident(X0,m)
| point_equal(X0,c)
| ~ incident(X0,r) ) ),
introduced(definition,[new_symbols(definition,[spl3_764])],[avatar_definition]) ).
fof(f6886,plain,
( ! [X0] :
( ~ incident(X0,r)
| point_equal(X0,c)
| ~ incident(X0,m) )
| ~ spl3_764 ),
inference(avatar_component_clause,[],[f6885]) ).
fof(f6887,plain,
( spl3_763
| spl3_764
| ~ spl3_760 ),
inference(avatar_split_clause,[],[f6869,f6844,f6885,f6881]) ).
fof(f6897,plain,
( incident(f,r)
| ~ spl3_763 ),
inference(resolution,[],[f6883,f110]) ).
fof(f6930,plain,
( point_equal(i,d)
| ~ incident(i,m)
| ~ spl3_310 ),
inference(resolution,[],[f2375,f2315]) ).
fof(f6939,plain,
( ! [X0] :
( ~ incident(X0,m)
| ~ incident(X0,r)
| point_equal(X0,d) )
| spl3_763 ),
inference(forward_subsumption_resolution,[],[f2396,f6882]) ).
fof(f6940,plain,
( spl3_310
| spl3_763 ),
inference(avatar_split_clause,[],[f6939,f6881,f2374]) ).
fof(f6942,plain,
( ! [X0] :
( ~ incident(f,X0)
| incident(i,X0) )
| ~ spl3_482 ),
inference(resolution,[],[f3569,f81]) ).
fof(f6962,plain,
( incident(i,l)
| ~ spl3_160
| ~ spl3_482 ),
inference(resolution,[],[f6942,f1292]) ).
fof(f6964,plain,
( incident(i,n)
| ~ spl3_482 ),
inference(resolution,[],[f6942,f120]) ).
fof(f6990,plain,
( $false
| spl3_481
| ~ spl3_482 ),
inference(forward_subsumption_resolution,[],[f6964,f3565]) ).
fof(f6991,plain,
( spl3_481
| ~ spl3_482 ),
inference(avatar_contradiction_clause,[],[f6990]) ).
fof(f7018,plain,
( incident(h,s)
| ~ spl3_238 ),
inference(resolution,[],[f1883,f137]) ).
fof(f7025,plain,
( $false
| spl3_189
| ~ spl3_238 ),
inference(forward_subsumption_resolution,[],[f7018,f1520]) ).
fof(f7026,plain,
( spl3_189
| ~ spl3_238 ),
inference(avatar_contradiction_clause,[],[f7025]) ).
fof(f7060,plain,
( ! [X0] :
( ~ incident(d,X0)
| incident(g,X0) )
| ~ spl3_516
| ~ spl3_590 ),
inference(resolution,[],[f5198,f81]) ).
fof(f7067,plain,
( incident(g,r)
| ~ spl3_516
| ~ spl3_590 ),
inference(resolution,[],[f7060,f2316]) ).
fof(f7191,plain,
( point_equal(f,a)
| ~ incident(f,l)
| ~ spl3_229 ),
inference(resolution,[],[f1763,f1504]) ).
fof(f7197,plain,
( point_equal(f,a)
| ~ spl3_160
| ~ spl3_229 ),
inference(forward_subsumption_resolution,[],[f7191,f1292]) ).
fof(f7205,plain,
( spl3_726
| ~ spl3_160
| ~ spl3_229 ),
inference(avatar_split_clause,[],[f7197,f1762,f1291,f6606]) ).
fof(f7219,plain,
( spl3_757
| ~ spl3_228 ),
inference(avatar_split_clause,[],[f1777,f1758,f6774]) ).
fof(f7222,plain,
( point_equal(a,f)
| ~ spl3_726 ),
inference(resolution,[],[f6608,f76]) ).
fof(f7223,plain,
( $false
| spl3_486
| ~ spl3_726 ),
inference(forward_subsumption_resolution,[],[f7222,f3618]) ).
fof(f7224,plain,
( spl3_486
| ~ spl3_726 ),
inference(avatar_contradiction_clause,[],[f7223]) ).
fof(f7225,plain,
( ! [X0] :
( ~ incident(X0,l)
| ~ incident(X0,r)
| line_equal(l,r)
| point_equal(X0,i) )
| ~ spl3_757 ),
inference(resolution,[],[f6775,f2320]) ).
fof(f7233,definition,
( spl3_784
<=> ! [X0] :
( ~ incident(X0,l)
| point_equal(X0,i)
| ~ incident(X0,r) ) ),
introduced(definition,[new_symbols(definition,[spl3_784])],[avatar_definition]) ).
fof(f7234,plain,
( ! [X0] :
( ~ incident(X0,r)
| point_equal(X0,i)
| ~ incident(X0,l) )
| ~ spl3_784 ),
inference(avatar_component_clause,[],[f7233]) ).
fof(f7235,plain,
( spl3_504
| spl3_784
| ~ spl3_757 ),
inference(avatar_split_clause,[],[f7225,f6774,f7233,f4061]) ).
fof(f7238,plain,
( point_equal(a,c)
| ~ spl3_728 ),
inference(resolution,[],[f6617,f76]) ).
fof(f7254,plain,
( spl3_504
| spl3_306 ),
inference(avatar_split_clause,[],[f2475,f2352,f4061]) ).
fof(f7299,plain,
( point_equal(c,a)
| ~ incident(c,l)
| ~ spl3_71
| ~ spl3_727 ),
inference(resolution,[],[f6612,f711]) ).
fof(f7315,plain,
( incident(g,s)
| ~ spl3_496
| ~ spl3_506 ),
inference(resolution,[],[f3912,f5366]) ).
fof(f7324,plain,
( incident(a,r)
| ~ spl3_504 ),
inference(resolution,[],[f4063,f98]) ).
fof(f7336,plain,
( ! [X0] :
( ~ incident(b,X0)
| incident(h,X0) )
| ~ spl3_616 ),
inference(resolution,[],[f5284,f81]) ).
fof(f7341,plain,
( incident(h,n)
| ~ spl3_616 ),
inference(resolution,[],[f7336,f121]) ).
fof(f7356,plain,
( incident(h,sK1(b,i))
| ~ point_equal(b,b)
| ~ spl3_10
| ~ spl3_616 ),
inference(resolution,[],[f7336,f1566]) ).
fof(f7357,plain,
( ~ point_equal(b,b)
| ~ spl3_10
| spl3_532
| ~ spl3_616 ),
inference(forward_subsumption_resolution,[],[f7356,f4558]) ).
fof(f7371,plain,
( $false
| spl3_615
| ~ spl3_616 ),
inference(forward_subsumption_resolution,[],[f7341,f5280]) ).
fof(f7372,plain,
( spl3_615
| ~ spl3_616 ),
inference(avatar_contradiction_clause,[],[f7371]) ).
fof(f7377,plain,
( $false
| ~ spl3_10
| spl3_532
| ~ spl3_616 ),
inference(forward_subsumption_resolution,[],[f7357,f102]) ).
fof(f7378,plain,
( ~ spl3_10
| spl3_532
| ~ spl3_616 ),
inference(avatar_contradiction_clause,[],[f7377]) ).
fof(f7884,plain,
( point_equal(a,f)
| ~ incident(a,l)
| ~ spl3_497 ),
inference(resolution,[],[f3915,f1505]) ).
fof(f7895,plain,
( ~ incident(a,l)
| spl3_486
| ~ spl3_497 ),
inference(forward_subsumption_resolution,[],[f7884,f3618]) ).
fof(f7904,plain,
( $false
| spl3_486
| ~ spl3_497 ),
inference(forward_subsumption_resolution,[],[f7895,f97]) ).
fof(f7905,plain,
( spl3_486
| ~ spl3_497 ),
inference(avatar_contradiction_clause,[],[f7904]) ).
fof(f7907,plain,
( point_equal(h,b)
| ~ spl3_161
| ~ spl3_499 ),
inference(resolution,[],[f4462,f5418]) ).
fof(f8706,plain,
( point_equal(a,i)
| ~ incident(a,r)
| ~ spl3_304 ),
inference(resolution,[],[f2339,f1505]) ).
fof(f8708,plain,
( point_equal(f,i)
| ~ incident(f,r)
| ~ spl3_304 ),
inference(resolution,[],[f2339,f1504]) ).
fof(f8709,plain,
( point_equal(g,i)
| ~ incident(g,r)
| ~ spl3_188
| ~ spl3_304 ),
inference(resolution,[],[f2339,f1515]) ).
fof(f8721,plain,
( point_equal(g,i)
| ~ spl3_188
| ~ spl3_301
| ~ spl3_304 ),
inference(forward_subsumption_resolution,[],[f8709,f2326]) ).
fof(f8722,plain,
( point_equal(f,i)
| ~ spl3_2
| ~ spl3_304
| ~ spl3_516 ),
inference(forward_subsumption_resolution,[],[f8708,f5230]) ).
fof(f8724,plain,
( point_equal(a,i)
| ~ spl3_304
| ~ spl3_504 ),
inference(forward_subsumption_resolution,[],[f8706,f7324]) ).
fof(f8770,plain,
( ! [X0] :
( ~ incident(i,X0)
| incident(g,X0) )
| ~ spl3_188
| ~ spl3_301
| ~ spl3_304 ),
inference(resolution,[],[f8721,f81]) ).
fof(f8801,plain,
( incident(g,sK1(i,h))
| ~ point_equal(i,i)
| ~ spl3_188
| ~ spl3_301
| ~ spl3_304 ),
inference(resolution,[],[f8770,f206]) ).
fof(f8804,plain,
( ~ point_equal(i,i)
| spl3_9
| ~ spl3_188
| ~ spl3_301
| ~ spl3_304 ),
inference(forward_subsumption_resolution,[],[f8801,f223]) ).
fof(f8817,plain,
( $false
| spl3_9
| ~ spl3_10
| ~ spl3_188
| ~ spl3_301
| ~ spl3_304 ),
inference(forward_subsumption_resolution,[],[f8804,f226]) ).
fof(f8818,plain,
( spl3_9
| ~ spl3_10
| ~ spl3_188
| ~ spl3_301
| ~ spl3_304 ),
inference(avatar_contradiction_clause,[],[f8817]) ).
fof(f8822,plain,
( point_equal(c,e)
| ~ spl3_18
| ~ spl3_760 ),
inference(forward_subsumption_resolution,[],[f4838,f6845]) ).
fof(f8823,plain,
( spl3_506
| ~ spl3_27 ),
inference(avatar_split_clause,[],[f397,f382,f4098]) ).
fof(f8829,plain,
( spl3_507
| ~ spl3_27 ),
inference(avatar_split_clause,[],[f682,f382,f4102]) ).
fof(f8835,plain,
( point_equal(b,g)
| ~ spl3_520 ),
inference(forward_subsumption_resolution,[],[f5788,f121]) ).
fof(f8848,definition,
( spl3_981
<=> point_equal(d,c) ),
introduced(definition,[new_symbols(definition,[spl3_981])],[avatar_definition]) ).
fof(f8849,plain,
( ~ point_equal(d,c)
| spl3_981 ),
inference(avatar_component_clause,[],[f8848]) ).
fof(f8850,plain,
( point_equal(d,c)
| ~ spl3_981 ),
inference(avatar_component_clause,[],[f8848]) ).
fof(f8854,plain,
( point_equal(c,d)
| ~ spl3_312
| ~ spl3_523 ),
inference(forward_subsumption_resolution,[],[f6211,f4476]) ).
fof(f8859,plain,
( $false
| spl3_301
| ~ spl3_516
| ~ spl3_590 ),
inference(forward_subsumption_resolution,[],[f7067,f2327]) ).
fof(f8860,plain,
( spl3_301
| ~ spl3_516
| ~ spl3_590 ),
inference(avatar_contradiction_clause,[],[f8859]) ).
fof(f8863,plain,
( $false
| ~ spl3_161
| spl3_264
| ~ spl3_520 ),
inference(forward_subsumption_resolution,[],[f5782,f2095]) ).
fof(f8864,plain,
( ~ spl3_161
| spl3_264
| ~ spl3_520 ),
inference(avatar_contradiction_clause,[],[f8863]) ).
fof(f8890,plain,
( spl3_69
| ~ spl3_1 ),
inference(avatar_split_clause,[],[f2038,f159,f676]) ).
fof(f8891,plain,
( spl3_264
| ~ spl3_4 ),
inference(avatar_split_clause,[],[f315,f174,f2093]) ).
fof(f8892,plain,
( ~ spl3_160
| spl3_161
| ~ spl3_28 ),
inference(avatar_split_clause,[],[f1287,f386,f1295,f1291]) ).
fof(f8901,plain,
( $false
| ~ spl3_18
| ~ spl3_264
| spl3_725 ),
inference(forward_subsumption_resolution,[],[f4852,f6604]) ).
fof(f8902,plain,
( ~ spl3_18
| ~ spl3_264
| spl3_725 ),
inference(avatar_contradiction_clause,[],[f8901]) ).
fof(f8913,definition,
( spl3_982
<=> incident(f,r) ),
introduced(definition,[new_symbols(definition,[spl3_982])],[avatar_definition]) ).
fof(f8915,plain,
( ~ incident(f,r)
| spl3_982 ),
inference(avatar_component_clause,[],[f8913]) ).
fof(f8917,definition,
( spl3_983
<=> point_equal(f,i) ),
introduced(definition,[new_symbols(definition,[spl3_983])],[avatar_definition]) ).
fof(f8919,plain,
( point_equal(f,i)
| ~ spl3_983 ),
inference(avatar_component_clause,[],[f8917]) ).
fof(f8920,plain,
( ~ spl3_982
| spl3_983
| ~ spl3_304 ),
inference(avatar_split_clause,[],[f8708,f2338,f8917,f8913]) ).
fof(f8939,plain,
( point_equal(h,d)
| ~ spl3_51
| ~ spl3_258 ),
inference(forward_subsumption_resolution,[],[f6369,f1998]) ).
fof(f8958,plain,
( point_equal(g,e)
| ~ spl3_68 ),
inference(resolution,[],[f674,f76]) ).
fof(f8999,plain,
( ! [X0] :
( ~ incident(e,X0)
| incident(g,X0) )
| ~ spl3_68 ),
inference(resolution,[],[f8958,f81]) ).
fof(f9018,definition,
( spl3_986
<=> line_equal(m,q) ),
introduced(definition,[new_symbols(definition,[spl3_986])],[avatar_definition]) ).
fof(f9020,plain,
( line_equal(m,q)
| ~ spl3_986 ),
inference(avatar_component_clause,[],[f9018]) ).
fof(f9028,plain,
( ! [X0] :
( ~ incident(a,X0)
| incident(i,X0) )
| ~ spl3_722 ),
inference(resolution,[],[f6590,f81]) ).
fof(f9034,plain,
( ! [X0] :
( ~ incident(h,X0)
| incident(e,X0) )
| ~ spl3_109 ),
inference(resolution,[],[f949,f81]) ).
fof(f9040,plain,
( ! [X0] :
( ~ incident(e,X0)
| incident(h,X0) )
| ~ spl3_259 ),
inference(resolution,[],[f2003,f81]) ).
fof(f9043,plain,
( ! [X0] :
( ~ incident(d,X0)
| incident(i,X0) )
| ~ spl3_673 ),
inference(resolution,[],[f6224,f81]) ).
fof(f9094,plain,
( point_equal(g,b)
| ~ spl3_520 ),
inference(resolution,[],[f8835,f76]) ).
fof(f9095,plain,
( $false
| spl3_508
| ~ spl3_520 ),
inference(forward_subsumption_resolution,[],[f9094,f4108]) ).
fof(f9096,plain,
( spl3_508
| ~ spl3_520 ),
inference(avatar_contradiction_clause,[],[f9095]) ).
fof(f9114,definition,
( spl3_988
<=> incident(a,r) ),
introduced(definition,[new_symbols(definition,[spl3_988])],[avatar_definition]) ).
fof(f9115,plain,
( incident(a,r)
| ~ spl3_988 ),
inference(avatar_component_clause,[],[f9114]) ).
fof(f9116,plain,
( ~ incident(a,r)
| spl3_988 ),
inference(avatar_component_clause,[],[f9114]) ).
fof(f9118,definition,
( spl3_989
<=> point_equal(a,i) ),
introduced(definition,[new_symbols(definition,[spl3_989])],[avatar_definition]) ).
fof(f9120,plain,
( point_equal(a,i)
| ~ spl3_989 ),
inference(avatar_component_clause,[],[f9118]) ).
fof(f9121,plain,
( ~ spl3_988
| spl3_989
| ~ spl3_304 ),
inference(avatar_split_clause,[],[f8706,f2338,f9118,f9114]) ).
fof(f9123,plain,
( incident(g,m)
| ~ spl3_68 ),
inference(resolution,[],[f8999,f108]) ).
fof(f9126,plain,
( incident(g,q)
| ~ spl3_68 ),
inference(resolution,[],[f8999,f132]) ).
fof(f9136,plain,
( incident(g,sK1(e,i))
| ~ point_equal(e,e)
| ~ spl3_10
| ~ spl3_68 ),
inference(resolution,[],[f8999,f1566]) ).
fof(f9137,plain,
( ~ point_equal(e,e)
| ~ spl3_10
| ~ spl3_68
| spl3_471 ),
inference(forward_subsumption_resolution,[],[f9136,f3413]) ).
fof(f9148,plain,
( $false
| ~ spl3_10
| ~ spl3_68
| spl3_471 ),
inference(forward_subsumption_resolution,[],[f9137,f114]) ).
fof(f9149,plain,
( ~ spl3_10
| ~ spl3_68
| spl3_471 ),
inference(avatar_contradiction_clause,[],[f9148]) ).
fof(f9171,plain,
( ! [X0] :
( ~ incident(c,X0)
| incident(d,X0) )
| ~ spl3_981 ),
inference(resolution,[],[f8850,f81]) ).
fof(f9173,plain,
( point_equal(c,d)
| ~ spl3_981 ),
inference(resolution,[],[f8850,f76]) ).
fof(f9174,plain,
( incident(d,l)
| ~ spl3_981 ),
inference(resolution,[],[f9171,f95]) ).
fof(f9197,plain,
( $false
| spl3_399
| ~ spl3_981 ),
inference(forward_subsumption_resolution,[],[f9174,f2903]) ).
fof(f9198,plain,
( spl3_399
| ~ spl3_981 ),
inference(avatar_contradiction_clause,[],[f9197]) ).
fof(f9212,plain,
( ! [X0] :
( ~ incident(i,X0)
| incident(f,X0) )
| ~ spl3_983 ),
inference(resolution,[],[f8919,f81]) ).
fof(f9214,plain,
( point_equal(i,f)
| ~ spl3_983 ),
inference(resolution,[],[f8919,f76]) ).
fof(f9217,plain,
( point_equal(i,a)
| ~ spl3_989 ),
inference(resolution,[],[f9120,f76]) ).
fof(f9249,plain,
( incident(f,l)
| ~ spl3_757
| ~ spl3_983 ),
inference(resolution,[],[f9212,f6775]) ).
fof(f9251,plain,
( incident(f,o)
| ~ spl3_262
| ~ spl3_983 ),
inference(resolution,[],[f9212,f2085]) ).
fof(f9275,plain,
( $false
| spl3_160
| ~ spl3_757
| ~ spl3_983 ),
inference(forward_subsumption_resolution,[],[f9249,f1293]) ).
fof(f9276,plain,
( spl3_160
| ~ spl3_757
| ~ spl3_983 ),
inference(avatar_contradiction_clause,[],[f9275]) ).
fof(f9293,plain,
( incident(i,l)
| ~ spl3_722 ),
inference(resolution,[],[f9028,f97]) ).
fof(f9294,plain,
( incident(i,q)
| ~ spl3_722 ),
inference(resolution,[],[f9028,f133]) ).
fof(f9314,plain,
( $false
| spl3_721
| ~ spl3_722 ),
inference(forward_subsumption_resolution,[],[f9294,f6586]) ).
fof(f9315,plain,
( spl3_721
| ~ spl3_722 ),
inference(avatar_contradiction_clause,[],[f9314]) ).
fof(f9316,plain,
( $false
| ~ spl3_722
| spl3_757 ),
inference(forward_subsumption_resolution,[],[f9293,f6776]) ).
fof(f9317,plain,
( ~ spl3_722
| spl3_757 ),
inference(avatar_contradiction_clause,[],[f9316]) ).
fof(f9318,plain,
( $false
| spl3_722
| ~ spl3_989 ),
inference(forward_subsumption_resolution,[],[f9217,f6589]) ).
fof(f9319,plain,
( spl3_722
| ~ spl3_989 ),
inference(avatar_contradiction_clause,[],[f9318]) ).
fof(f9396,plain,
( spl3_258
| ~ spl3_7 ),
inference(avatar_split_clause,[],[f198,f191,f1997]) ).
fof(f9405,plain,
( spl3_762
| ~ spl3_224 ),
inference(avatar_split_clause,[],[f1770,f1729,f6853]) ).
fof(f9411,plain,
( spl3_986
| spl3_8 ),
inference(avatar_split_clause,[],[f6262,f195,f9018]) ).
fof(f9414,plain,
( ~ incident(a,m)
| ~ spl3_225
| spl3_486 ),
inference(forward_subsumption_resolution,[],[f6822,f3618]) ).
fof(f9419,plain,
( $false
| ~ spl3_48
| spl3_617 ),
inference(forward_subsumption_resolution,[],[f564,f5289]) ).
fof(f9420,plain,
( ~ spl3_48
| spl3_617 ),
inference(avatar_contradiction_clause,[],[f9419]) ).
fof(f9430,plain,
( spl3_399
| ~ spl3_308
| ~ spl3_489 ),
inference(avatar_split_clause,[],[f5093,f3677,f2360,f2901]) ).
fof(f9434,plain,
( spl3_502
| spl3_49 ),
inference(avatar_split_clause,[],[f600,f525,f4053]) ).
fof(f9437,plain,
( point_equal(h,a)
| ~ spl3_71
| ~ spl3_617 ),
inference(forward_subsumption_resolution,[],[f5724,f5288]) ).
fof(f9457,plain,
( incident(e,l)
| ~ spl3_109
| ~ spl3_617 ),
inference(resolution,[],[f5288,f9034]) ).
fof(f9478,plain,
( spl3_612
| ~ spl3_109
| ~ spl3_617 ),
inference(avatar_split_clause,[],[f9457,f5287,f947,f5262]) ).
fof(f9479,plain,
( point_equal(e,a)
| ~ spl3_71
| ~ spl3_612 ),
inference(forward_subsumption_resolution,[],[f5723,f5263]) ).
fof(f9480,plain,
( ! [X0] :
( ~ incident(c,X0)
| incident(e,X0) )
| ~ spl3_614 ),
inference(resolution,[],[f5274,f81]) ).
fof(f9522,plain,
( incident(e,l)
| ~ spl3_614 ),
inference(resolution,[],[f9480,f95]) ).
fof(f9525,plain,
( incident(e,p)
| ~ spl3_523
| ~ spl3_614 ),
inference(resolution,[],[f9480,f4476]) ).
fof(f9575,plain,
( ! [X0] :
( ~ incident(e,X0)
| incident(c,X0) )
| ~ spl3_614 ),
inference(resolution,[],[f6574,f81]) ).
fof(f9579,plain,
( incident(c,m)
| ~ spl3_614 ),
inference(resolution,[],[f9575,f108]) ).
fof(f9582,plain,
( incident(c,q)
| ~ spl3_614 ),
inference(resolution,[],[f9575,f132]) ).
fof(f9643,plain,
( incident(h,o)
| ~ spl3_259 ),
inference(resolution,[],[f9040,f258]) ).
fof(f9655,plain,
( incident(h,sK1(e,i))
| ~ point_equal(e,e)
| ~ spl3_10
| ~ spl3_259 ),
inference(resolution,[],[f9040,f1566]) ).
fof(f9656,plain,
( incident(h,sK1(e,i))
| ~ spl3_10
| ~ spl3_259 ),
inference(forward_subsumption_resolution,[],[f9655,f114]) ).
fof(f9668,plain,
( spl3_472
| ~ spl3_10
| ~ spl3_259 ),
inference(avatar_split_clause,[],[f9656,f2001,f225,f3415]) ).
fof(f9730,plain,
( incident(i,p)
| ~ spl3_673 ),
inference(resolution,[],[f9043,f509]) ).
fof(f9784,plain,
( point_equal(a,e)
| ~ spl3_71
| ~ spl3_612 ),
inference(resolution,[],[f9479,f76]) ).
fof(f9787,plain,
( $false
| spl3_612
| ~ spl3_614 ),
inference(forward_subsumption_resolution,[],[f9522,f5264]) ).
fof(f9788,plain,
( spl3_612
| ~ spl3_614 ),
inference(avatar_contradiction_clause,[],[f9787]) ).
fof(f9789,plain,
( $false
| spl3_108
| ~ spl3_523
| ~ spl3_614 ),
inference(forward_subsumption_resolution,[],[f9525,f945]) ).
fof(f9790,plain,
( spl3_108
| ~ spl3_523
| ~ spl3_614 ),
inference(avatar_contradiction_clause,[],[f9789]) ).
fof(f9813,plain,
( incident(g,r)
| ~ spl3_328 ),
inference(resolution,[],[f2496,f278]) ).
fof(f9820,plain,
( $false
| spl3_301
| ~ spl3_328 ),
inference(forward_subsumption_resolution,[],[f9813,f2327]) ).
fof(f9821,plain,
( spl3_301
| ~ spl3_328 ),
inference(avatar_contradiction_clause,[],[f9820]) ).
fof(f9825,plain,
( ! [X0] :
( ~ incident(a,X0)
| incident(h,X0) )
| ~ spl3_71
| ~ spl3_617 ),
inference(resolution,[],[f9437,f81]) ).
fof(f9832,definition,
( spl3_999
<=> point_equal(c,e) ),
introduced(definition,[new_symbols(definition,[spl3_999])],[avatar_definition]) ).
fof(f9834,plain,
( point_equal(c,e)
| ~ spl3_999 ),
inference(avatar_component_clause,[],[f9832]) ).
fof(f9844,plain,
( point_equal(d,b)
| ~ spl3_257 ),
inference(forward_subsumption_resolution,[],[f6795,f109]) ).
fof(f9853,plain,
( $false
| spl3_482
| ~ spl3_983 ),
inference(forward_subsumption_resolution,[],[f9214,f3568]) ).
fof(f9854,plain,
( spl3_482
| ~ spl3_983 ),
inference(avatar_contradiction_clause,[],[f9853]) ).
fof(f10048,plain,
( point_equal(e,c)
| ~ spl3_999 ),
inference(resolution,[],[f9834,f76]) ).
fof(f10049,plain,
( $false
| spl3_614
| ~ spl3_999 ),
inference(forward_subsumption_resolution,[],[f10048,f5273]) ).
fof(f10050,plain,
( spl3_614
| ~ spl3_999 ),
inference(avatar_contradiction_clause,[],[f10049]) ).
fof(f10081,plain,
( point_equal(d,c)
| ~ spl3_306
| ~ spl3_399 ),
inference(forward_subsumption_resolution,[],[f6768,f2902]) ).
fof(f10088,plain,
( $false
| ~ spl3_262
| spl3_264
| ~ spl3_983 ),
inference(forward_subsumption_resolution,[],[f9251,f2095]) ).
fof(f10089,plain,
( ~ spl3_262
| spl3_264
| ~ spl3_983 ),
inference(avatar_contradiction_clause,[],[f10088]) ).
fof(f10090,plain,
( point_equal(i,d)
| ~ spl3_310
| ~ spl3_762 ),
inference(forward_subsumption_resolution,[],[f6930,f6854]) ).
fof(f10095,plain,
( spl3_612
| ~ spl3_261 ),
inference(avatar_split_clause,[],[f3816,f2059,f5262]) ).
fof(f10096,plain,
( $false
| spl3_260
| ~ spl3_261 ),
inference(forward_subsumption_resolution,[],[f3713,f2057]) ).
fof(f10097,plain,
( spl3_260
| ~ spl3_261 ),
inference(avatar_contradiction_clause,[],[f10096]) ).
fof(f10099,plain,
( spl3_760
| ~ spl3_309 ),
inference(avatar_split_clause,[],[f2387,f2370,f6844]) ).
fof(f10104,plain,
( spl3_727
| ~ spl3_614 ),
inference(avatar_split_clause,[],[f9582,f5272,f6611]) ).
fof(f10105,plain,
( spl3_760
| ~ spl3_614 ),
inference(avatar_split_clause,[],[f9579,f5272,f6844]) ).
fof(f10107,plain,
( point_equal(c,a)
| ~ spl3_71
| ~ spl3_727 ),
inference(forward_subsumption_resolution,[],[f7299,f95]) ).
fof(f10111,plain,
( spl3_999
| ~ spl3_18
| ~ spl3_760 ),
inference(avatar_split_clause,[],[f8822,f6844,f270,f9832]) ).
fof(f10112,plain,
( point_equal(e,b)
| ~ spl3_53
| ~ spl3_612 ),
inference(forward_subsumption_resolution,[],[f2123,f5263]) ).
fof(f10124,plain,
( spl3_519
| ~ spl3_259 ),
inference(avatar_split_clause,[],[f9643,f2001,f4398]) ).
fof(f10131,definition,
( spl3_1000
<=> point_equal(c,d) ),
introduced(definition,[new_symbols(definition,[spl3_1000])],[avatar_definition]) ).
fof(f10133,plain,
( point_equal(c,d)
| ~ spl3_1000 ),
inference(avatar_component_clause,[],[f10131]) ).
fof(f10137,plain,
( spl3_989
| ~ spl3_304
| ~ spl3_504 ),
inference(avatar_split_clause,[],[f8724,f4061,f2338,f9118]) ).
fof(f10318,plain,
( spl3_189
| ~ spl3_107 ),
inference(avatar_split_clause,[],[f3518,f938,f1518]) ).
fof(f10319,plain,
( spl3_617
| ~ spl3_107 ),
inference(avatar_split_clause,[],[f3514,f938,f5287]) ).
fof(f10323,plain,
( spl3_981
| ~ spl3_306
| ~ spl3_399 ),
inference(avatar_split_clause,[],[f10081,f2901,f2352,f8848]) ).
fof(f10331,plain,
( spl3_1000
| ~ spl3_981 ),
inference(avatar_split_clause,[],[f9173,f8848,f10131]) ).
fof(f10334,plain,
( point_equal(h,i)
| ~ incident(h,r)
| ~ spl3_189
| ~ spl3_304 ),
inference(resolution,[],[f1519,f2339]) ).
fof(f10406,plain,
( ! [X0] :
( ~ incident(d,X0)
| incident(c,X0) )
| ~ spl3_1000 ),
inference(resolution,[],[f10133,f81]) ).
fof(f10471,plain,
( incident(c,m)
| ~ spl3_1000 ),
inference(resolution,[],[f10406,f109]) ).
fof(f10473,plain,
( incident(c,p)
| ~ spl3_1000 ),
inference(resolution,[],[f10406,f509]) ).
fof(f10498,plain,
( spl3_723
| ~ spl3_68 ),
inference(avatar_split_clause,[],[f9126,f672,f6593]) ).
fof(f10513,plain,
( $false
| ~ spl3_763
| spl3_982 ),
inference(forward_subsumption_resolution,[],[f6897,f8915]) ).
fof(f10514,plain,
( ~ spl3_763
| spl3_982 ),
inference(avatar_contradiction_clause,[],[f10513]) ).
fof(f10515,plain,
( $false
| spl3_523
| ~ spl3_1000 ),
inference(forward_subsumption_resolution,[],[f10473,f4477]) ).
fof(f10516,plain,
( spl3_523
| ~ spl3_1000 ),
inference(avatar_contradiction_clause,[],[f10515]) ).
fof(f10534,plain,
( spl3_673
| ~ spl3_310
| ~ spl3_762 ),
inference(avatar_split_clause,[],[f10090,f6853,f2374,f6222]) ).
fof(f10535,plain,
( $false
| spl3_188
| ~ spl3_496
| ~ spl3_506 ),
inference(forward_subsumption_resolution,[],[f7315,f1516]) ).
fof(f10536,plain,
( spl3_188
| ~ spl3_496
| ~ spl3_506 ),
inference(avatar_contradiction_clause,[],[f10535]) ).
fof(f10542,plain,
( $false
| spl3_672
| ~ spl3_673 ),
inference(forward_subsumption_resolution,[],[f9730,f6220]) ).
fof(f10543,plain,
( spl3_672
| ~ spl3_673 ),
inference(avatar_contradiction_clause,[],[f10542]) ).
fof(f10544,plain,
( spl3_757
| ~ spl3_722 ),
inference(avatar_split_clause,[],[f9293,f6588,f6774]) ).
fof(f10551,definition,
( spl3_1007
<=> point_equal(e,b) ),
introduced(definition,[new_symbols(definition,[spl3_1007])],[avatar_definition]) ).
fof(f10553,plain,
( point_equal(e,b)
| ~ spl3_1007 ),
inference(avatar_component_clause,[],[f10551]) ).
fof(f10575,plain,
( spl3_520
| ~ spl3_5
| ~ spl3_489 ),
inference(avatar_split_clause,[],[f5756,f3677,f179,f4403]) ).
fof(f10580,plain,
( $false
| spl3_260
| ~ spl3_486 ),
inference(forward_subsumption_resolution,[],[f4248,f2057]) ).
fof(f10581,plain,
( spl3_260
| ~ spl3_486 ),
inference(avatar_contradiction_clause,[],[f10580]) ).
fof(f10582,plain,
( $false
| ~ spl3_27
| spl3_160 ),
inference(forward_subsumption_resolution,[],[f399,f1293]) ).
fof(f10583,plain,
( ~ spl3_27
| spl3_160 ),
inference(avatar_contradiction_clause,[],[f10582]) ).
fof(f10732,definition,
( spl3_1008
<=> incident(g,p) ),
introduced(definition,[new_symbols(definition,[spl3_1008])],[avatar_definition]) ).
fof(f10733,plain,
( incident(g,p)
| ~ spl3_1008 ),
inference(avatar_component_clause,[],[f10732]) ).
fof(f10734,plain,
( ~ incident(g,p)
| spl3_1008 ),
inference(avatar_component_clause,[],[f10732]) ).
fof(f10741,plain,
( ~ incident(i,l)
| ~ spl3_306
| spl3_758 ),
inference(forward_subsumption_resolution,[],[f6770,f6779]) ).
fof(f10746,plain,
( spl3_1000
| ~ spl3_312
| ~ spl3_523 ),
inference(avatar_split_clause,[],[f8854,f4475,f2382,f10131]) ).
fof(f10748,plain,
( $false
| spl3_760
| ~ spl3_1000 ),
inference(forward_subsumption_resolution,[],[f10471,f6846]) ).
fof(f10749,plain,
( spl3_760
| ~ spl3_1000 ),
inference(avatar_contradiction_clause,[],[f10748]) ).
fof(f10750,plain,
( $false
| spl3_3
| ~ spl3_68 ),
inference(forward_subsumption_resolution,[],[f9123,f172]) ).
fof(f10751,plain,
( spl3_3
| ~ spl3_68 ),
inference(avatar_contradiction_clause,[],[f10750]) ).
fof(f10761,plain,
( spl3_1008
| ~ spl3_508 ),
inference(avatar_split_clause,[],[f4299,f4107,f10732]) ).
fof(f10858,plain,
( point_equal(g,h)
| ~ incident(g,p)
| ~ spl3_77
| ~ spl3_723 ),
inference(resolution,[],[f6594,f748]) ).
fof(f11064,plain,
( incident(h,r)
| ~ spl3_71
| ~ spl3_617
| ~ spl3_988 ),
inference(resolution,[],[f9115,f9825]) ).
fof(f11081,plain,
( $false
| ~ spl3_71
| spl3_302
| ~ spl3_617
| ~ spl3_988 ),
inference(forward_subsumption_resolution,[],[f11064,f2331]) ).
fof(f11082,plain,
( ~ spl3_71
| spl3_302
| ~ spl3_617
| ~ spl3_988 ),
inference(avatar_contradiction_clause,[],[f11081]) ).
fof(f11083,plain,
( point_equal(h,i)
| ~ spl3_189
| ~ spl3_302
| ~ spl3_304 ),
inference(forward_subsumption_resolution,[],[f10334,f2330]) ).
fof(f11095,plain,
( ! [X0] :
( ~ incident(i,X0)
| incident(h,X0) )
| ~ spl3_189
| ~ spl3_302
| ~ spl3_304 ),
inference(resolution,[],[f11083,f81]) ).
fof(f11115,plain,
( incident(h,sK1(i,g))
| ~ point_equal(i,i)
| ~ spl3_189
| ~ spl3_302
| ~ spl3_304 ),
inference(resolution,[],[f11095,f406]) ).
fof(f11119,plain,
( ~ point_equal(i,i)
| spl3_31
| ~ spl3_189
| ~ spl3_302
| ~ spl3_304 ),
inference(forward_subsumption_resolution,[],[f11115,f435]) ).
fof(f11134,plain,
( $false
| ~ spl3_10
| spl3_31
| ~ spl3_189
| ~ spl3_302
| ~ spl3_304 ),
inference(forward_subsumption_resolution,[],[f11119,f226]) ).
fof(f11135,plain,
( ~ spl3_10
| spl3_31
| ~ spl3_189
| ~ spl3_302
| ~ spl3_304 ),
inference(avatar_contradiction_clause,[],[f11134]) ).
fof(f11163,plain,
( $false
| ~ spl3_24
| ~ spl3_70
| spl3_614 ),
inference(forward_subsumption_resolution,[],[f1266,f5273]) ).
fof(f11164,plain,
( ~ spl3_24
| ~ spl3_70
| spl3_614 ),
inference(avatar_contradiction_clause,[],[f11163]) ).
fof(f11170,plain,
( spl3_616
| ~ spl3_70
| ~ spl3_77 ),
inference(avatar_split_clause,[],[f2922,f747,f706,f5282]) ).
fof(f11175,plain,
( spl3_616
| ~ spl3_161
| ~ spl3_499 ),
inference(avatar_split_clause,[],[f7907,f3924,f1295,f5282]) ).
fof(f11177,plain,
( spl3_400
| ~ spl3_257 ),
inference(avatar_split_clause,[],[f9844,f1964,f2905]) ).
fof(f11181,plain,
( spl3_983
| ~ spl3_2
| ~ spl3_304
| ~ spl3_516 ),
inference(avatar_split_clause,[],[f8722,f4378,f2338,f163,f8917]) ).
fof(f11188,plain,
( spl3_1007
| ~ spl3_53
| ~ spl3_612 ),
inference(avatar_split_clause,[],[f10112,f5262,f559,f10551]) ).
fof(f11467,plain,
( ! [X0] :
( ~ incident(i,X0)
| incident(f,X0) )
| ~ spl3_983 ),
inference(resolution,[],[f8919,f81]) ).
fof(f11511,plain,
( incident(f,q)
| ~ spl3_721
| ~ spl3_983 ),
inference(resolution,[],[f11467,f6585]) ).
fof(f11587,plain,
( point_equal(b,e)
| ~ spl3_1007 ),
inference(resolution,[],[f10553,f76]) ).
fof(f11588,plain,
( spl3_521
| ~ spl3_1007 ),
inference(avatar_split_clause,[],[f11587,f10551,f4407]) ).
fof(f11602,plain,
( ~ incident(h,n)
| ~ incident(g,n)
| ~ spl3_481 ),
inference(resolution,[],[f3564,f94]) ).
fof(f11609,plain,
( ~ incident(g,n)
| ~ spl3_481
| ~ spl3_615 ),
inference(forward_subsumption_resolution,[],[f11602,f5279]) ).
fof(f11612,plain,
( $false
| ~ spl3_481
| ~ spl3_615 ),
inference(forward_subsumption_resolution,[],[f11609,f119]) ).
fof(f11613,plain,
( ~ spl3_481
| ~ spl3_615 ),
inference(avatar_contradiction_clause,[],[f11612]) ).
fof(f11632,plain,
( $false
| ~ spl3_10
| ~ spl3_23
| ~ spl3_28
| spl3_531 ),
inference(forward_subsumption_resolution,[],[f1607,f4554]) ).
fof(f11633,plain,
( ~ spl3_10
| ~ spl3_23
| ~ spl3_28
| spl3_531 ),
inference(avatar_contradiction_clause,[],[f11632]) ).
fof(f11638,plain,
( spl3_261
| ~ spl3_71
| ~ spl3_612 ),
inference(avatar_split_clause,[],[f9784,f5262,f710,f2059]) ).
fof(f11639,plain,
( spl3_728
| ~ spl3_71
| ~ spl3_727 ),
inference(avatar_split_clause,[],[f10107,f6611,f710,f6615]) ).
fof(f11644,plain,
( ~ spl3_757
| ~ spl3_306
| spl3_758 ),
inference(avatar_split_clause,[],[f10741,f6778,f2352,f6774]) ).
fof(f11948,plain,
( point_equal(a,e)
| ~ incident(a,m)
| ~ spl3_8 ),
inference(resolution,[],[f196,f133]) ).
fof(f12023,plain,
( incident(h,r)
| ~ spl3_313 ),
inference(resolution,[],[f2417,f512]) ).
fof(f12028,plain,
( $false
| spl3_302
| ~ spl3_313 ),
inference(forward_subsumption_resolution,[],[f12023,f2331]) ).
fof(f12029,plain,
( spl3_302
| ~ spl3_313 ),
inference(avatar_contradiction_clause,[],[f12028]) ).
fof(f12033,plain,
( ! [X0] :
( ~ incident(e,X0)
| incident(b,X0) )
| ~ spl3_521 ),
inference(resolution,[],[f4409,f81]) ).
fof(f12063,plain,
( ! [X0] :
( ~ incident(c,X0)
| incident(a,X0) )
| ~ spl3_728 ),
inference(resolution,[],[f7238,f81]) ).
fof(f12070,plain,
( incident(a,r)
| ~ spl3_728 ),
inference(resolution,[],[f12063,f2317]) ).
fof(f12089,plain,
( $false
| ~ spl3_728
| spl3_988 ),
inference(forward_subsumption_resolution,[],[f12070,f9116]) ).
fof(f12090,plain,
( ~ spl3_728
| spl3_988 ),
inference(avatar_contradiction_clause,[],[f12089]) ).
fof(f12100,plain,
( spl3_725
| ~ spl3_721
| ~ spl3_983 ),
inference(avatar_split_clause,[],[f11511,f8917,f6584,f6602]) ).
fof(f12140,plain,
( point_equal(f,h)
| ~ incident(f,p)
| ~ spl3_77
| ~ spl3_725 ),
inference(resolution,[],[f6603,f748]) ).
fof(f12249,plain,
( ~ spl3_260
| spl3_261
| ~ spl3_8 ),
inference(avatar_split_clause,[],[f11948,f195,f2059,f2055]) ).
fof(f12256,plain,
( ~ incident(e,l)
| ~ spl3_24
| spl3_614 ),
inference(forward_subsumption_resolution,[],[f1263,f5273]) ).
fof(f12270,plain,
( spl3_757
| ~ spl3_160
| ~ spl3_482 ),
inference(avatar_split_clause,[],[f6962,f3567,f1291,f6774]) ).
fof(f12274,plain,
( ~ spl3_260
| ~ spl3_225
| spl3_486 ),
inference(avatar_split_clause,[],[f9414,f3617,f1733,f2055]) ).
fof(f12282,plain,
( ~ incident(f,p)
| ~ spl3_77
| spl3_499
| ~ spl3_725 ),
inference(forward_subsumption_resolution,[],[f12140,f3925]) ).
fof(f12295,plain,
( $false
| ~ spl3_77
| ~ spl3_498
| spl3_499
| ~ spl3_725 ),
inference(forward_subsumption_resolution,[],[f12282,f3921]) ).
fof(f12296,plain,
( ~ spl3_77
| ~ spl3_498
| spl3_499
| ~ spl3_725 ),
inference(avatar_contradiction_clause,[],[f12295]) ).
fof(f12302,plain,
( ~ incident(f,q)
| ~ spl3_266
| spl3_726 ),
inference(forward_subsumption_resolution,[],[f6578,f6607]) ).
fof(f12423,plain,
( ! [X0] :
( ~ incident(c,X0)
| incident(i,X0) )
| ~ spl3_758 ),
inference(resolution,[],[f6780,f81]) ).
fof(f12524,plain,
( ~ incident(h,p)
| ~ incident(g,p)
| ~ spl3_672 ),
inference(resolution,[],[f6219,f94]) ).
fof(f12584,plain,
( spl3_1008
| ~ spl3_23
| ~ spl3_28 ),
inference(avatar_split_clause,[],[f1304,f386,f356,f10732]) ).
fof(f12591,plain,
( ~ incident(g,p)
| ~ spl3_672 ),
inference(forward_subsumption_resolution,[],[f12524,f508]) ).
fof(f12593,plain,
( $false
| ~ spl3_672
| ~ spl3_1008 ),
inference(forward_subsumption_resolution,[],[f12591,f10733]) ).
fof(f12594,plain,
( ~ spl3_672
| ~ spl3_1008 ),
inference(avatar_contradiction_clause,[],[f12593]) ).
fof(f12600,plain,
( ~ spl3_612
| ~ spl3_24
| spl3_614 ),
inference(avatar_split_clause,[],[f12256,f5272,f360,f5262]) ).
fof(f12690,plain,
( incident(b,o)
| ~ spl3_521 ),
inference(resolution,[],[f12033,f258]) ).
fof(f12710,plain,
( $false
| spl3_520
| ~ spl3_521 ),
inference(forward_subsumption_resolution,[],[f12690,f4405]) ).
fof(f12711,plain,
( spl3_520
| ~ spl3_521 ),
inference(avatar_contradiction_clause,[],[f12710]) ).
fof(f12737,plain,
( incident(f,q)
| ~ spl3_986 ),
inference(resolution,[],[f9020,f110]) ).
fof(f12740,plain,
( incident(a,n)
| ~ spl3_618 ),
inference(resolution,[],[f5356,f98]) ).
fof(f12749,plain,
( $false
| spl3_485
| ~ spl3_618 ),
inference(forward_subsumption_resolution,[],[f12740,f3615]) ).
fof(f12750,plain,
( spl3_485
| ~ spl3_618 ),
inference(avatar_contradiction_clause,[],[f12749]) ).
fof(f12838,plain,
( ! [X0] :
( ~ incident(d,X0)
| incident(h,X0) )
| ~ spl3_51
| ~ spl3_258 ),
inference(resolution,[],[f8939,f81]) ).
fof(f12843,plain,
( incident(h,r)
| ~ spl3_51
| ~ spl3_258 ),
inference(resolution,[],[f12838,f2316]) ).
fof(f12891,plain,
( ~ spl3_725
| ~ spl3_266
| spl3_726 ),
inference(avatar_split_clause,[],[f12302,f6606,f2146,f6602]) ).
fof(f12893,plain,
( $false
| spl3_725
| ~ spl3_986 ),
inference(forward_subsumption_resolution,[],[f12737,f6604]) ).
fof(f12894,plain,
( spl3_725
| ~ spl3_986 ),
inference(avatar_contradiction_clause,[],[f12893]) ).
fof(f13144,plain,
( incident(i,o)
| ~ spl3_758 ),
inference(resolution,[],[f12423,f259]) ).
fof(f13164,plain,
( $false
| spl3_262
| ~ spl3_758 ),
inference(forward_subsumption_resolution,[],[f13144,f2086]) ).
fof(f13165,plain,
( spl3_262
| ~ spl3_758 ),
inference(avatar_contradiction_clause,[],[f13164]) ).
fof(f13168,plain,
( ~ incident(h,o)
| ~ incident(g,o)
| ~ spl3_262 ),
inference(resolution,[],[f2085,f94]) ).
fof(f13175,plain,
( ~ incident(g,o)
| ~ spl3_262
| ~ spl3_519 ),
inference(forward_subsumption_resolution,[],[f13168,f4399]) ).
fof(f13176,plain,
( $false
| ~ spl3_262
| ~ spl3_519 ),
inference(forward_subsumption_resolution,[],[f13175,f257]) ).
fof(f13177,plain,
( ~ spl3_262
| ~ spl3_519 ),
inference(avatar_contradiction_clause,[],[f13176]) ).
fof(f13179,plain,
( spl3_302
| ~ spl3_51
| ~ spl3_258 ),
inference(avatar_split_clause,[],[f12843,f1997,f538,f2329]) ).
fof(f13181,plain,
( $false
| ~ spl3_58
| spl3_1008 ),
inference(forward_subsumption_resolution,[],[f632,f10734]) ).
fof(f13182,plain,
( ~ spl3_58
| spl3_1008 ),
inference(avatar_contradiction_clause,[],[f13181]) ).
fof(f13374,plain,
( spl3_516
| ~ spl3_1 ),
inference(avatar_split_clause,[],[f2037,f159,f4378]) ).
fof(f13380,plain,
( spl3_399
| ~ spl3_305 ),
inference(avatar_split_clause,[],[f2391,f2348,f2901]) ).
fof(f13388,definition,
( spl3_1040
<=> point_equal(g,h) ),
introduced(definition,[new_symbols(definition,[spl3_1040])],[avatar_definition]) ).
fof(f13390,plain,
( point_equal(g,h)
| ~ spl3_1040 ),
inference(avatar_component_clause,[],[f13388]) ).
fof(f13391,plain,
( ~ spl3_1008
| spl3_1040
| ~ spl3_77
| ~ spl3_723 ),
inference(avatar_split_clause,[],[f10858,f6593,f747,f13388,f10732]) ).
fof(f13563,plain,
( ! [X0] :
( ~ incident(h,X0)
| incident(g,X0) )
| ~ spl3_1040 ),
inference(resolution,[],[f13390,f81]) ).
fof(f13648,plain,
( ~ incident(h,q)
| ~ incident(g,q)
| ~ spl3_721 ),
inference(resolution,[],[f6585,f94]) ).
fof(f13657,plain,
( ~ incident(g,q)
| ~ spl3_721 ),
inference(forward_subsumption_resolution,[],[f13648,f131]) ).
fof(f13659,plain,
( $false
| ~ spl3_721
| ~ spl3_723 ),
inference(forward_subsumption_resolution,[],[f13657,f6594]) ).
fof(f13660,plain,
( ~ spl3_721
| ~ spl3_723 ),
inference(avatar_contradiction_clause,[],[f13659]) ).
fof(f13665,plain,
( $false
| spl3_399
| ~ spl3_400 ),
inference(forward_subsumption_resolution,[],[f5968,f2903]) ).
fof(f13666,plain,
( spl3_399
| ~ spl3_400 ),
inference(avatar_contradiction_clause,[],[f13665]) ).
fof(f13696,plain,
( incident(g,sK1(i,h))
| ~ spl3_10
| ~ spl3_1040 ),
inference(resolution,[],[f13563,f1567]) ).
fof(f13714,plain,
( $false
| spl3_9
| ~ spl3_10
| ~ spl3_1040 ),
inference(forward_subsumption_resolution,[],[f13696,f223]) ).
fof(f13715,plain,
( spl3_9
| ~ spl3_10
| ~ spl3_1040 ),
inference(avatar_contradiction_clause,[],[f13714]) ).
fof(f13725,plain,
( incident(a,p)
| ~ spl3_502 ),
inference(resolution,[],[f4055,f98]) ).
fof(f13726,plain,
( incident(c,p)
| ~ spl3_502 ),
inference(resolution,[],[f4055,f104]) ).
fof(f13732,plain,
( $false
| ~ spl3_502
| spl3_523 ),
inference(forward_subsumption_resolution,[],[f13726,f4477]) ).
fof(f13733,plain,
( ~ spl3_502
| spl3_523 ),
inference(avatar_contradiction_clause,[],[f13732]) ).
fof(f13734,plain,
( $false
| spl3_106
| ~ spl3_502 ),
inference(forward_subsumption_resolution,[],[f13725,f936]) ).
fof(f13735,plain,
( spl3_106
| ~ spl3_502 ),
inference(avatar_contradiction_clause,[],[f13734]) ).
fof(f13881,plain,
( point_equal(b,f)
| ~ incident(b,l)
| ~ spl3_619 ),
inference(resolution,[],[f5359,f121]) ).
fof(f13890,plain,
( ~ incident(b,l)
| spl3_6
| ~ spl3_619 ),
inference(forward_subsumption_resolution,[],[f13881,f184]) ).
fof(f13892,plain,
( $false
| spl3_6
| ~ spl3_619 ),
inference(forward_subsumption_resolution,[],[f13890,f96]) ).
fof(f13893,plain,
( spl3_6
| ~ spl3_619 ),
inference(avatar_contradiction_clause,[],[f13892]) ).
fof(f14649,plain,
( point_equal(g,f)
| ~ incident(g,n)
| ~ spl3_540 ),
inference(resolution,[],[f4626,f257]) ).
fof(f14658,plain,
( ~ incident(g,n)
| spl3_4
| ~ spl3_540 ),
inference(forward_subsumption_resolution,[],[f14649,f175]) ).
fof(f14659,plain,
( $false
| spl3_4
| ~ spl3_540 ),
inference(forward_subsumption_resolution,[],[f14658,f119]) ).
fof(f14660,plain,
( spl3_4
| ~ spl3_540 ),
inference(avatar_contradiction_clause,[],[f14659]) ).
fof(f14833,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ colinear(X2,e,X4,X8)
| incident(X1,m)
| incident(X2,m)
| incident(d,X3)
| incident(e,X3)
| incident(f,X3)
| ~ colinear(X0,X1,X2,X3)
| colinear(X4,X5,X6,sK0(X4,X5,X6))
| ~ colinear(X1,f,X4,X7)
| incident(X0,m)
| ~ colinear(X1,d,X5,X9)
| ~ colinear(X0,e,X5,X10)
| ~ colinear(X2,d,X6,X11)
| ~ colinear(X0,f,X6,X12) ),
inference(resolution,[],[f83,f60]) ).
fof(f14850,plain,
( point_equal(d,c)
| ~ incident(d,m)
| ~ spl3_764 ),
inference(resolution,[],[f6886,f2316]) ).
fof(f14861,plain,
( ~ incident(d,m)
| ~ spl3_764
| spl3_981 ),
inference(forward_subsumption_resolution,[],[f14850,f8849]) ).
fof(f14863,plain,
( $false
| ~ spl3_764
| spl3_981 ),
inference(forward_subsumption_resolution,[],[f14861,f109]) ).
fof(f14864,plain,
( ~ spl3_764
| spl3_981 ),
inference(avatar_contradiction_clause,[],[f14863]) ).
fof(f14928,plain,
( point_equal(c,i)
| ~ incident(c,l)
| ~ spl3_784 ),
inference(resolution,[],[f7234,f2317]) ).
fof(f14940,plain,
( point_equal(c,i)
| ~ spl3_784 ),
inference(forward_subsumption_resolution,[],[f14928,f95]) ).
fof(f14944,plain,
( point_equal(i,c)
| ~ spl3_784 ),
inference(resolution,[],[f14940,f76]) ).
fof(f14945,plain,
( $false
| spl3_758
| ~ spl3_784 ),
inference(forward_subsumption_resolution,[],[f14944,f6779]) ).
fof(f14946,plain,
( spl3_758
| ~ spl3_784 ),
inference(avatar_contradiction_clause,[],[f14945]) ).
fof(f15023,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( incident(X0,m)
| incident(c,m)
| incident(d,X1)
| incident(e,X1)
| incident(f,X1)
| ~ colinear(X2,X0,c,X1)
| colinear(g,X3,X4,sK0(g,X3,X4))
| ~ colinear(X0,f,g,X5)
| incident(X2,m)
| ~ colinear(X0,d,X3,X6)
| ~ colinear(X2,e,X3,X7)
| ~ colinear(c,d,X4,X8)
| ~ colinear(X2,f,X4,X9) ),
inference(resolution,[],[f14833,f62]) ).
fof(f15025,plain,
( ! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ colinear(c,d,X4,X8)
| incident(d,X1)
| incident(e,X1)
| incident(f,X1)
| ~ colinear(X2,X0,c,X1)
| colinear(g,X3,X4,sK0(g,X3,X4))
| ~ colinear(X0,f,g,X5)
| incident(X2,m)
| ~ colinear(X0,d,X3,X6)
| ~ colinear(X2,e,X3,X7)
| incident(X0,m)
| ~ colinear(X2,f,X4,X9) )
| spl3_760 ),
inference(forward_subsumption_resolution,[],[f15023,f6846]) ).
fof(f15027,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ colinear(X2,f,g,X4)
| incident(e,X0)
| incident(f,X0)
| ~ colinear(X1,X2,c,X0)
| colinear(g,X3,i,sK0(g,X3,i))
| incident(d,X0)
| incident(X1,m)
| ~ colinear(X2,d,X3,X5)
| ~ colinear(X1,e,X3,X6)
| incident(X2,m)
| ~ colinear(X1,f,i,X7) )
| spl3_760 ),
inference(resolution,[],[f15025,f67]) ).
fof(f16371,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( incident(e,X0)
| incident(f,X0)
| ~ colinear(X1,b,c,X0)
| colinear(g,X2,i,sK0(g,X2,i))
| incident(d,X0)
| incident(X1,m)
| ~ colinear(b,d,X2,X3)
| ~ colinear(X1,e,X2,X4)
| incident(b,m)
| ~ colinear(X1,f,i,X5) )
| spl3_760 ),
inference(resolution,[],[f15027,f63]) ).
fof(f16372,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ colinear(b,d,X2,X3)
| incident(f,X0)
| ~ colinear(X1,b,c,X0)
| colinear(g,X2,i,sK0(g,X2,i))
| incident(d,X0)
| incident(X1,m)
| incident(e,X0)
| ~ colinear(X1,e,X2,X4)
| ~ colinear(X1,f,i,X5) )
| spl3_5
| spl3_760 ),
inference(forward_subsumption_resolution,[],[f16371,f181]) ).
fof(f16373,plain,
( ! [X2,X3,X0,X1] :
( incident(f,X0)
| ~ colinear(X1,b,c,X0)
| colinear(g,h,i,sK0(g,h,i))
| incident(d,X0)
| incident(X1,m)
| incident(e,X0)
| ~ colinear(X1,e,h,X2)
| ~ colinear(X1,f,i,X3) )
| spl3_5
| spl3_760 ),
inference(resolution,[],[f16372,f65]) ).
fof(f16375,definition,
( spl3_1374
<=> colinear(g,h,i,sK0(g,h,i)) ),
introduced(definition,[new_symbols(definition,[spl3_1374])],[avatar_definition]) ).
fof(f16377,plain,
( colinear(g,h,i,sK0(g,h,i))
| ~ spl3_1374 ),
inference(avatar_component_clause,[],[f16375]) ).
fof(f16379,definition,
( spl3_1375
<=> ! [X0,X3,X2,X1] :
( incident(f,X0)
| ~ colinear(X1,f,i,X3)
| ~ colinear(X1,e,h,X2)
| incident(e,X0)
| incident(X1,m)
| incident(d,X0)
| ~ colinear(X1,b,c,X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_1375])],[avatar_definition]) ).
fof(f16380,plain,
( ! [X2,X3,X0,X1] :
( ~ colinear(X1,f,i,X3)
| incident(f,X0)
| ~ colinear(X1,e,h,X2)
| incident(e,X0)
| incident(X1,m)
| incident(d,X0)
| ~ colinear(X1,b,c,X0) )
| ~ spl3_1375 ),
inference(avatar_component_clause,[],[f16379]) ).
fof(f16381,plain,
( spl3_1374
| spl3_1375
| spl3_5
| spl3_760 ),
inference(avatar_split_clause,[],[f16373,f6844,f179,f16379,f16375]) ).
fof(f16382,plain,
( ! [X0,X1] :
( incident(f,X0)
| ~ colinear(a,e,h,X1)
| incident(e,X0)
| incident(a,m)
| incident(d,X0)
| ~ colinear(a,b,c,X0) )
| ~ spl3_1375 ),
inference(resolution,[],[f16380,f66]) ).
fof(f16383,plain,
( ! [X0,X1] :
( incident(f,X0)
| ~ colinear(a,e,h,X1)
| incident(e,X0)
| incident(d,X0)
| ~ colinear(a,b,c,X0) )
| spl3_260
| ~ spl3_1375 ),
inference(forward_subsumption_resolution,[],[f16382,f2057]) ).
fof(f16385,definition,
( spl3_1376
<=> ! [X1] : ~ colinear(a,e,h,X1) ),
introduced(definition,[new_symbols(definition,[spl3_1376])],[avatar_definition]) ).
fof(f16386,plain,
( ! [X1] : ~ colinear(a,e,h,X1)
| ~ spl3_1376 ),
inference(avatar_component_clause,[],[f16385]) ).
fof(f16388,definition,
( spl3_1377
<=> ! [X0] :
( incident(f,X0)
| ~ colinear(a,b,c,X0)
| incident(d,X0)
| incident(e,X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_1377])],[avatar_definition]) ).
fof(f16389,plain,
( ! [X0] :
( ~ colinear(a,b,c,X0)
| incident(f,X0)
| incident(d,X0)
| incident(e,X0) )
| ~ spl3_1377 ),
inference(avatar_component_clause,[],[f16388]) ).
fof(f16391,plain,
( incident(f,l)
| incident(d,l)
| incident(e,l)
| ~ spl3_1377 ),
inference(resolution,[],[f16389,f61]) ).
fof(f16392,plain,
( incident(d,l)
| incident(e,l)
| spl3_160
| ~ spl3_1377 ),
inference(forward_subsumption_resolution,[],[f16391,f1293]) ).
fof(f16393,plain,
( incident(e,l)
| spl3_160
| spl3_399
| ~ spl3_1377 ),
inference(forward_subsumption_resolution,[],[f16392,f2903]) ).
fof(f16394,plain,
( $false
| spl3_160
| spl3_399
| spl3_612
| ~ spl3_1377 ),
inference(forward_subsumption_resolution,[],[f16393,f5264]) ).
fof(f16395,plain,
( spl3_160
| spl3_399
| spl3_612
| ~ spl3_1377 ),
inference(avatar_contradiction_clause,[],[f16394]) ).
fof(f16397,plain,
( incident(i,sK0(g,h,i))
| ~ spl3_1374 ),
inference(resolution,[],[f16377,f74]) ).
fof(f16398,plain,
( incident(h,sK0(g,h,i))
| ~ spl3_1374 ),
inference(resolution,[],[f16377,f73]) ).
fof(f16399,plain,
( incident(g,sK0(g,h,i))
| ~ spl3_1374 ),
inference(resolution,[],[f16377,f72]) ).
fof(f16424,plain,
( ~ incident(h,sK0(g,h,i))
| ~ incident(g,sK0(g,h,i))
| ~ spl3_1374 ),
inference(resolution,[],[f16397,f94]) ).
fof(f16429,plain,
( ~ incident(g,sK0(g,h,i))
| ~ spl3_1374 ),
inference(forward_subsumption_resolution,[],[f16424,f16398]) ).
fof(f16446,plain,
( $false
| ~ spl3_1374 ),
inference(forward_subsumption_resolution,[],[f16429,f16399]) ).
fof(f16447,plain,
~ spl3_1374,
inference(avatar_contradiction_clause,[],[f16446]) ).
fof(f16449,plain,
( spl3_1376
| spl3_1377
| spl3_260
| ~ spl3_1375 ),
inference(avatar_split_clause,[],[f16383,f16379,f2055,f16388,f16385]) ).
fof(f16450,plain,
( $false
| ~ spl3_1376 ),
inference(resolution,[],[f16386,f64]) ).
fof(f16451,plain,
~ spl3_1376,
inference(avatar_contradiction_clause,[],[f16450]) ).
cnf(s1,plain,
( spl3_1
| spl3_2 ),
inference(sat_conversion,[],[f165]) ).
cnf(s4,plain,
( spl3_7
| spl3_8 ),
inference(sat_conversion,[],[f197]) ).
cnf(s5,plain,
( ~ spl3_9
| ~ spl3_10 ),
inference(sat_conversion,[],[f228]) ).
cnf(s9,plain,
( spl3_17
| spl3_18 ),
inference(sat_conversion,[],[f272]) ).
cnf(s10,plain,
( spl3_3
| ~ spl3_17 ),
inference(sat_conversion,[],[f287]) ).
cnf(s14,plain,
( spl3_23
| spl3_24 ),
inference(sat_conversion,[],[f362]) ).
cnf(s16,plain,
( spl3_27
| spl3_28 ),
inference(sat_conversion,[],[f388]) ).
cnf(s18,plain,
( ~ spl3_10
| ~ spl3_31 ),
inference(sat_conversion,[],[f436]) ).
cnf(s27,plain,
( spl3_48
| spl3_49 ),
inference(sat_conversion,[],[f527]) ).
cnf(s28,plain,
( spl3_50
| spl3_51 ),
inference(sat_conversion,[],[f540]) ).
cnf(s29,plain,
( spl3_5
| ~ spl3_50 ),
inference(sat_conversion,[],[f547]) ).
cnf(s30,plain,
( ~ spl3_1
| spl3_5 ),
inference(sat_conversion,[],[f548]) ).
cnf(s31,plain,
( ~ spl3_5
| spl3_52
| spl3_53 ),
inference(sat_conversion,[],[f561]) ).
cnf(s36,plain,
( spl3_58
| spl3_59 ),
inference(sat_conversion,[],[f615]) ).
cnf(s41,plain,
( spl3_68
| ~ spl3_69 ),
inference(sat_conversion,[],[f679]) ).
cnf(s42,plain,
( spl3_70
| spl3_71 ),
inference(sat_conversion,[],[f712]) ).
cnf(s45,plain,
( spl3_76
| spl3_77 ),
inference(sat_conversion,[],[f749]) ).
cnf(s48,plain,
~ spl3_76,
inference(sat_conversion,[],[f772]) ).
cnf(s61,plain,
( ~ spl3_77
| ~ spl3_106
| spl3_107 ),
inference(sat_conversion,[],[f941]) ).
cnf(s62,plain,
( ~ spl3_77
| ~ spl3_108
| spl3_109 ),
inference(sat_conversion,[],[f950]) ).
cnf(s104,plain,
spl3_10,
inference(sat_conversion,[],[f1512]) ).
cnf(s105,plain,
( ~ spl3_188
| ~ spl3_189 ),
inference(sat_conversion,[],[f1521]) ).
cnf(s123,plain,
( spl3_224
| spl3_225 ),
inference(sat_conversion,[],[f1735]) ).
cnf(s126,plain,
( spl3_228
| spl3_229 ),
inference(sat_conversion,[],[f1764]) ).
cnf(s142,plain,
( ~ spl3_5
| spl3_256
| spl3_257 ),
inference(sat_conversion,[],[f1966]) ).
cnf(s150,plain,
( ~ spl3_6
| spl3_161 ),
inference(sat_conversion,[],[f2066]) ).
cnf(s152,plain,
( spl3_108
| ~ spl3_256 ),
inference(sat_conversion,[],[f2078]) ).
cnf(s155,plain,
( spl3_238
| spl3_266 ),
inference(sat_conversion,[],[f2148]) ).
cnf(s174,plain,
( ~ spl3_301
| ~ spl3_302 ),
inference(sat_conversion,[],[f2332]) ).
cnf(s176,plain,
( spl3_305
| spl3_306 ),
inference(sat_conversion,[],[f2354]) ).
cnf(s178,plain,
( spl3_309
| spl3_310 ),
inference(sat_conversion,[],[f2376]) ).
cnf(s180,plain,
( spl3_312
| spl3_313 ),
inference(sat_conversion,[],[f2418]) ).
cnf(s188,plain,
( spl3_308
| spl3_328 ),
inference(sat_conversion,[],[f2497]) ).
cnf(s204,plain,
spl3_304,
inference(sat_conversion,[],[f2630]) ).
cnf(s230,plain,
( ~ spl3_48
| ~ spl3_70 ),
inference(sat_conversion,[],[f2899]) ).
cnf(s269,plain,
( ~ spl3_10
| ~ spl3_471
| ~ spl3_472 ),
inference(sat_conversion,[],[f3418]) ).
cnf(s289,plain,
( spl3_3
| ~ spl3_4 ),
inference(sat_conversion,[],[f3628]) ).
cnf(s290,plain,
( ~ spl3_4
| spl3_188 ),
inference(sat_conversion,[],[f3629]) ).
cnf(s302,plain,
( spl3_69
| ~ spl3_261
| ~ spl3_485 ),
inference(sat_conversion,[],[f3840]) ).
cnf(s305,plain,
( ~ spl3_2
| ~ spl3_5
| spl3_6 ),
inference(sat_conversion,[],[f3853]) ).
cnf(s309,plain,
( spl3_160
| ~ spl3_161 ),
inference(sat_conversion,[],[f3892]) ).
cnf(s311,plain,
( ~ spl3_160
| spl3_496
| spl3_497 ),
inference(sat_conversion,[],[f3916]) ).
cnf(s314,plain,
( ~ spl3_161
| spl3_498 ),
inference(sat_conversion,[],[f3928]) ).
cnf(s319,plain,
( ~ spl3_53
| spl3_106
| ~ spl3_260 ),
inference(sat_conversion,[],[f4039]) ).
cnf(s320,plain,
( ~ spl3_52
| spl3_399 ),
inference(sat_conversion,[],[f4041]) ).
cnf(s324,plain,
( ~ spl3_28
| spl3_106
| ~ spl3_485 ),
inference(sat_conversion,[],[f4095]) ).
cnf(s335,plain,
( ~ spl3_2
| ~ spl3_3
| spl3_4 ),
inference(sat_conversion,[],[f4211]) ).
cnf(s339,plain,
( spl3_485
| ~ spl3_486 ),
inference(sat_conversion,[],[f4271]) ).
cnf(s344,plain,
( ~ spl3_59
| spl3_400
| ~ spl3_516 ),
inference(sat_conversion,[],[f4381]) ).
cnf(s359,plain,
( ~ spl3_10
| ~ spl3_531
| ~ spl3_532 ),
inference(sat_conversion,[],[f4559]) ).
cnf(s366,plain,
( ~ spl3_264
| spl3_539
| spl3_540 ),
inference(sat_conversion,[],[f4627]) ).
cnf(s376,plain,
~ spl3_539,
inference(sat_conversion,[],[f4707]) ).
cnf(s393,plain,
( spl3_18
| spl3_489 ),
inference(sat_conversion,[],[f4878]) ).
cnf(s398,plain,
( ~ spl3_3
| spl3_589
| spl3_590 ),
inference(sat_conversion,[],[f4970]) ).
cnf(s408,plain,
( spl3_1
| ~ spl3_589 ),
inference(sat_conversion,[],[f5050]) ).
cnf(s417,plain,
( ~ spl3_49
| ~ spl3_399
| spl3_400 ),
inference(sat_conversion,[],[f5126]) ).
cnf(s418,plain,
( ~ spl3_400
| spl3_516 ),
inference(sat_conversion,[],[f5153]) ).
cnf(s421,plain,
( ~ spl3_2
| spl3_160
| ~ spl3_399
| ~ spl3_516 ),
inference(sat_conversion,[],[f5252]) ).
cnf(s427,plain,
( spl3_6
| ~ spl3_161 ),
inference(sat_conversion,[],[f5258]) ).
cnf(s430,plain,
( ~ spl3_400
| spl3_516 ),
inference(sat_conversion,[],[f5260]) ).
cnf(s436,plain,
( spl3_5
| ~ spl3_6 ),
inference(sat_conversion,[],[f5292]) ).
cnf(s438,plain,
( ~ spl3_160
| spl3_618
| spl3_619 ),
inference(sat_conversion,[],[f5360]) ).
cnf(s442,plain,
( spl3_301
| ~ spl3_507 ),
inference(sat_conversion,[],[f5611]) ).
cnf(s450,plain,
( ~ spl3_109
| spl3_259 ),
inference(sat_conversion,[],[f5800]) ).
cnf(s549,plain,
( ~ spl3_760
| spl3_763
| spl3_764 ),
inference(sat_conversion,[],[f6887]) ).
cnf(s555,plain,
( spl3_310
| spl3_763 ),
inference(sat_conversion,[],[f6940]) ).
cnf(s558,plain,
( spl3_481
| ~ spl3_482 ),
inference(sat_conversion,[],[f6991]) ).
cnf(s566,plain,
( spl3_189
| ~ spl3_238 ),
inference(sat_conversion,[],[f7026]) ).
cnf(s581,plain,
( ~ spl3_160
| ~ spl3_229
| spl3_726 ),
inference(sat_conversion,[],[f7205]) ).
cnf(s590,plain,
( ~ spl3_228
| spl3_757 ),
inference(sat_conversion,[],[f7219]) ).
cnf(s592,plain,
( spl3_486
| ~ spl3_726 ),
inference(sat_conversion,[],[f7224]) ).
cnf(s593,plain,
( spl3_504
| ~ spl3_757
| spl3_784 ),
inference(sat_conversion,[],[f7235]) ).
cnf(s597,plain,
( spl3_306
| spl3_504 ),
inference(sat_conversion,[],[f7254]) ).
cnf(s605,plain,
( spl3_615
| ~ spl3_616 ),
inference(sat_conversion,[],[f7372]) ).
cnf(s608,plain,
( ~ spl3_10
| spl3_532
| ~ spl3_616 ),
inference(sat_conversion,[],[f7378]) ).
cnf(s664,plain,
( spl3_486
| ~ spl3_497 ),
inference(sat_conversion,[],[f7905]) ).
cnf(s758,plain,
( spl3_9
| ~ spl3_10
| ~ spl3_188
| ~ spl3_301
| ~ spl3_304 ),
inference(sat_conversion,[],[f8818]) ).
cnf(s761,plain,
( ~ spl3_27
| spl3_506 ),
inference(sat_conversion,[],[f8823]) ).
cnf(s766,plain,
( ~ spl3_27
| spl3_507 ),
inference(sat_conversion,[],[f8829]) ).
cnf(s776,plain,
( spl3_301
| ~ spl3_516
| ~ spl3_590 ),
inference(sat_conversion,[],[f8860]) ).
cnf(s777,plain,
( ~ spl3_161
| spl3_264
| ~ spl3_520 ),
inference(sat_conversion,[],[f8864]) ).
cnf(s788,plain,
( ~ spl3_1
| spl3_69 ),
inference(sat_conversion,[],[f8890]) ).
cnf(s790,plain,
( ~ spl3_4
| spl3_264 ),
inference(sat_conversion,[],[f8891]) ).
cnf(s794,plain,
( ~ spl3_28
| ~ spl3_160
| spl3_161 ),
inference(sat_conversion,[],[f8892]) ).
cnf(s800,plain,
( ~ spl3_18
| ~ spl3_264
| spl3_725 ),
inference(sat_conversion,[],[f8902]) ).
cnf(s802,plain,
( ~ spl3_304
| ~ spl3_982
| spl3_983 ),
inference(sat_conversion,[],[f8920]) ).
cnf(s819,plain,
( spl3_508
| ~ spl3_520 ),
inference(sat_conversion,[],[f9096]) ).
cnf(s825,plain,
( ~ spl3_304
| ~ spl3_988
| spl3_989 ),
inference(sat_conversion,[],[f9121]) ).
cnf(s829,plain,
( ~ spl3_10
| ~ spl3_68
| spl3_471 ),
inference(sat_conversion,[],[f9149]) ).
cnf(s830,plain,
( spl3_399
| ~ spl3_981 ),
inference(sat_conversion,[],[f9198]) ).
cnf(s833,plain,
( spl3_160
| ~ spl3_757
| ~ spl3_983 ),
inference(sat_conversion,[],[f9276]) ).
cnf(s835,plain,
( spl3_721
| ~ spl3_722 ),
inference(sat_conversion,[],[f9315]) ).
cnf(s836,plain,
( ~ spl3_722
| spl3_757 ),
inference(sat_conversion,[],[f9317]) ).
cnf(s837,plain,
( spl3_722
| ~ spl3_989 ),
inference(sat_conversion,[],[f9319]) ).
cnf(s839,plain,
( ~ spl3_7
| spl3_258 ),
inference(sat_conversion,[],[f9396]) ).
cnf(s847,plain,
( ~ spl3_224
| spl3_762 ),
inference(sat_conversion,[],[f9405]) ).
cnf(s852,plain,
( spl3_8
| spl3_986 ),
inference(sat_conversion,[],[f9411]) ).
cnf(s854,plain,
( ~ spl3_48
| spl3_617 ),
inference(sat_conversion,[],[f9420]) ).
cnf(s858,plain,
( ~ spl3_308
| spl3_399
| ~ spl3_489 ),
inference(sat_conversion,[],[f9430]) ).
cnf(s860,plain,
( spl3_49
| spl3_502 ),
inference(sat_conversion,[],[f9434]) ).
cnf(s866,plain,
( ~ spl3_109
| spl3_612
| ~ spl3_617 ),
inference(sat_conversion,[],[f9478]) ).
cnf(s874,plain,
( ~ spl3_10
| ~ spl3_259
| spl3_472 ),
inference(sat_conversion,[],[f9668]) ).
cnf(s881,plain,
( spl3_612
| ~ spl3_614 ),
inference(sat_conversion,[],[f9788]) ).
cnf(s882,plain,
( spl3_108
| ~ spl3_523
| ~ spl3_614 ),
inference(sat_conversion,[],[f9790]) ).
cnf(s884,plain,
( spl3_301
| ~ spl3_328 ),
inference(sat_conversion,[],[f9821]) ).
cnf(s913,plain,
( spl3_482
| ~ spl3_983 ),
inference(sat_conversion,[],[f9854]) ).
cnf(s925,plain,
( spl3_614
| ~ spl3_999 ),
inference(sat_conversion,[],[f10050]) ).
cnf(s932,plain,
( ~ spl3_262
| spl3_264
| ~ spl3_983 ),
inference(sat_conversion,[],[f10089]) ).
cnf(s935,plain,
( ~ spl3_261
| spl3_612 ),
inference(sat_conversion,[],[f10095]) ).
cnf(s936,plain,
( spl3_260
| ~ spl3_261 ),
inference(sat_conversion,[],[f10097]) ).
cnf(s938,plain,
( ~ spl3_309
| spl3_760 ),
inference(sat_conversion,[],[f10099]) ).
cnf(s945,plain,
( ~ spl3_614
| spl3_727 ),
inference(sat_conversion,[],[f10104]) ).
cnf(s946,plain,
( ~ spl3_614
| spl3_760 ),
inference(sat_conversion,[],[f10105]) ).
cnf(s952,plain,
( ~ spl3_18
| ~ spl3_760
| spl3_999 ),
inference(sat_conversion,[],[f10111]) ).
cnf(s961,plain,
( ~ spl3_259
| spl3_519 ),
inference(sat_conversion,[],[f10124]) ).
cnf(s970,plain,
( ~ spl3_304
| ~ spl3_504
| spl3_989 ),
inference(sat_conversion,[],[f10137]) ).
cnf(s977,plain,
( ~ spl3_107
| spl3_189 ),
inference(sat_conversion,[],[f10318]) ).
cnf(s978,plain,
( ~ spl3_107
| spl3_617 ),
inference(sat_conversion,[],[f10319]) ).
cnf(s985,plain,
( ~ spl3_306
| ~ spl3_399
| spl3_981 ),
inference(sat_conversion,[],[f10323]) ).
cnf(s990,plain,
( ~ spl3_981
| spl3_1000 ),
inference(sat_conversion,[],[f10331]) ).
cnf(s1009,plain,
( ~ spl3_68
| spl3_723 ),
inference(sat_conversion,[],[f10498]) ).
cnf(s1023,plain,
( ~ spl3_763
| spl3_982 ),
inference(sat_conversion,[],[f10514]) ).
cnf(s1024,plain,
( spl3_523
| ~ spl3_1000 ),
inference(sat_conversion,[],[f10516]) ).
cnf(s1042,plain,
( ~ spl3_310
| spl3_673
| ~ spl3_762 ),
inference(sat_conversion,[],[f10534]) ).
cnf(s1044,plain,
( spl3_188
| ~ spl3_496
| ~ spl3_506 ),
inference(sat_conversion,[],[f10536]) ).
cnf(s1050,plain,
( spl3_672
| ~ spl3_673 ),
inference(sat_conversion,[],[f10543]) ).
cnf(s1052,plain,
( ~ spl3_722
| spl3_757 ),
inference(sat_conversion,[],[f10544]) ).
cnf(s1078,plain,
( ~ spl3_5
| ~ spl3_489
| spl3_520 ),
inference(sat_conversion,[],[f10575]) ).
cnf(s1088,plain,
( spl3_260
| ~ spl3_486 ),
inference(sat_conversion,[],[f10581]) ).
cnf(s1089,plain,
( ~ spl3_27
| spl3_160 ),
inference(sat_conversion,[],[f10583]) ).
cnf(s1148,plain,
( ~ spl3_312
| ~ spl3_523
| spl3_1000 ),
inference(sat_conversion,[],[f10746]) ).
cnf(s1155,plain,
( spl3_760
| ~ spl3_1000 ),
inference(sat_conversion,[],[f10749]) ).
cnf(s1156,plain,
( spl3_3
| ~ spl3_68 ),
inference(sat_conversion,[],[f10751]) ).
cnf(s1169,plain,
( ~ spl3_508
| spl3_1008 ),
inference(sat_conversion,[],[f10761]) ).
cnf(s1185,plain,
( ~ spl3_71
| spl3_302
| ~ spl3_617
| ~ spl3_988 ),
inference(sat_conversion,[],[f11082]) ).
cnf(s1194,plain,
( ~ spl3_10
| spl3_31
| ~ spl3_189
| ~ spl3_302
| ~ spl3_304 ),
inference(sat_conversion,[],[f11135]) ).
cnf(s1225,plain,
( ~ spl3_24
| ~ spl3_70
| spl3_614 ),
inference(sat_conversion,[],[f11164]) ).
cnf(s1229,plain,
( ~ spl3_70
| ~ spl3_77
| spl3_616 ),
inference(sat_conversion,[],[f11170]) ).
cnf(s1236,plain,
( ~ spl3_161
| ~ spl3_499
| spl3_616 ),
inference(sat_conversion,[],[f11175]) ).
cnf(s1241,plain,
( ~ spl3_257
| spl3_400 ),
inference(sat_conversion,[],[f11177]) ).
cnf(s1256,plain,
( ~ spl3_2
| ~ spl3_304
| ~ spl3_516
| spl3_983 ),
inference(sat_conversion,[],[f11181]) ).
cnf(s1268,plain,
( ~ spl3_53
| ~ spl3_612
| spl3_1007 ),
inference(sat_conversion,[],[f11188]) ).
cnf(s1278,plain,
( spl3_521
| ~ spl3_1007 ),
inference(sat_conversion,[],[f11588]) ).
cnf(s1279,plain,
( ~ spl3_481
| ~ spl3_615 ),
inference(sat_conversion,[],[f11613]) ).
cnf(s1289,plain,
( ~ spl3_10
| ~ spl3_23
| ~ spl3_28
| spl3_531 ),
inference(sat_conversion,[],[f11633]) ).
cnf(s1293,plain,
( ~ spl3_71
| spl3_261
| ~ spl3_612 ),
inference(sat_conversion,[],[f11638]) ).
cnf(s1294,plain,
( ~ spl3_71
| ~ spl3_727
| spl3_728 ),
inference(sat_conversion,[],[f11639]) ).
cnf(s1309,plain,
( ~ spl3_306
| ~ spl3_757
| spl3_758 ),
inference(sat_conversion,[],[f11644]) ).
cnf(s1324,plain,
( spl3_302
| ~ spl3_313 ),
inference(sat_conversion,[],[f12029]) ).
cnf(s1328,plain,
( ~ spl3_728
| spl3_988 ),
inference(sat_conversion,[],[f12090]) ).
cnf(s1342,plain,
( ~ spl3_721
| spl3_725
| ~ spl3_983 ),
inference(sat_conversion,[],[f12100]) ).
cnf(s1366,plain,
( ~ spl3_8
| ~ spl3_260
| spl3_261 ),
inference(sat_conversion,[],[f12249]) ).
cnf(s1381,plain,
( ~ spl3_160
| ~ spl3_482
| spl3_757 ),
inference(sat_conversion,[],[f12270]) ).
cnf(s1389,plain,
( ~ spl3_225
| ~ spl3_260
| spl3_486 ),
inference(sat_conversion,[],[f12274]) ).
cnf(s1404,plain,
( ~ spl3_77
| ~ spl3_498
| spl3_499
| ~ spl3_725 ),
inference(sat_conversion,[],[f12296]) ).
cnf(s1427,plain,
( ~ spl3_23
| ~ spl3_28
| spl3_1008 ),
inference(sat_conversion,[],[f12584]) ).
cnf(s1449,plain,
( ~ spl3_672
| ~ spl3_1008 ),
inference(sat_conversion,[],[f12594]) ).
cnf(s1450,plain,
( ~ spl3_24
| ~ spl3_612
| spl3_614 ),
inference(sat_conversion,[],[f12600]) ).
cnf(s1456,plain,
( spl3_520
| ~ spl3_521 ),
inference(sat_conversion,[],[f12711]) ).
cnf(s1462,plain,
( spl3_485
| ~ spl3_618 ),
inference(sat_conversion,[],[f12750]) ).
cnf(s1528,plain,
( ~ spl3_266
| ~ spl3_725
| spl3_726 ),
inference(sat_conversion,[],[f12891]) ).
cnf(s1530,plain,
( spl3_725
| ~ spl3_986 ),
inference(sat_conversion,[],[f12894]) ).
cnf(s1537,plain,
( spl3_262
| ~ spl3_758 ),
inference(sat_conversion,[],[f13165]) ).
cnf(s1538,plain,
( ~ spl3_262
| ~ spl3_519 ),
inference(sat_conversion,[],[f13177]) ).
cnf(s1539,plain,
( ~ spl3_51
| ~ spl3_258
| spl3_302 ),
inference(sat_conversion,[],[f13179]) ).
cnf(s1541,plain,
( ~ spl3_58
| spl3_1008 ),
inference(sat_conversion,[],[f13182]) ).
cnf(s1571,plain,
( ~ spl3_1
| spl3_516 ),
inference(sat_conversion,[],[f13374]) ).
cnf(s1583,plain,
( ~ spl3_305
| spl3_399 ),
inference(sat_conversion,[],[f13380]) ).
cnf(s1616,plain,
( ~ spl3_77
| ~ spl3_723
| ~ spl3_1008
| spl3_1040 ),
inference(sat_conversion,[],[f13391]) ).
cnf(s1619,plain,
( ~ spl3_721
| ~ spl3_723 ),
inference(sat_conversion,[],[f13660]) ).
cnf(s1627,plain,
( spl3_399
| ~ spl3_400 ),
inference(sat_conversion,[],[f13666]) ).
cnf(s1646,plain,
( spl3_9
| ~ spl3_10
| ~ spl3_1040 ),
inference(sat_conversion,[],[f13715]) ).
cnf(s1653,plain,
( ~ spl3_502
| spl3_523 ),
inference(sat_conversion,[],[f13733]) ).
cnf(s1654,plain,
( spl3_106
| ~ spl3_502 ),
inference(sat_conversion,[],[f13735]) ).
cnf(s1669,plain,
( spl3_6
| ~ spl3_619 ),
inference(sat_conversion,[],[f13893]) ).
cnf(s1745,plain,
( spl3_4
| ~ spl3_540 ),
inference(sat_conversion,[],[f14660]) ).
cnf(s1761,plain,
( ~ spl3_764
| spl3_981 ),
inference(sat_conversion,[],[f14864]) ).
cnf(s1770,plain,
( spl3_758
| ~ spl3_784 ),
inference(sat_conversion,[],[f14946]) ).
cnf(s1893,plain,
( spl3_5
| spl3_760
| spl3_1374
| spl3_1375 ),
inference(sat_conversion,[],[f16381]) ).
cnf(s1895,plain,
( spl3_160
| spl3_399
| spl3_612
| ~ spl3_1377 ),
inference(sat_conversion,[],[f16395]) ).
cnf(s1900,plain,
~ spl3_1374,
inference(sat_conversion,[],[f16447]) ).
cnf(s1901,plain,
( spl3_260
| ~ spl3_1375
| spl3_1376
| spl3_1377 ),
inference(sat_conversion,[],[f16449]) ).
cnf(s1902,plain,
~ spl3_1376,
inference(sat_conversion,[],[f16451]) ).
cnf(s1903,plain,
( spl3_260
| ~ spl3_1375
| spl3_1377 ),
inference(rat,[],[s1901,s1902]) ).
cnf(s1905,plain,
( spl3_5
| spl3_760
| spl3_1375 ),
inference(rat,[],[s1893,s1900]) ).
cnf(s1925,plain,
( ~ spl3_264
| spl3_540 ),
inference(rat,[],[s366,s376]) ).
cnf(s1929,plain,
spl3_77,
inference(rat,[],[s45,s48]) ).
cnf(s1931,plain,
~ spl3_31,
inference(rat,[],[s18,s104]) ).
cnf(s1932,plain,
~ spl3_9,
inference(rat,[],[s5,s104]) ).
cnf(s1933,plain,
~ spl3_1040,
inference(rat,[],[s1646,s104,s1932]) ).
cnf(s1934,plain,
( spl3_260
| ~ spl3_71
| spl3_399
| spl3_160
| spl3_5
| ~ spl3_18 ),
inference(rat,[],[s1905,s952,s1903,s925,s1895,s881,s1293,s936]) ).
cnf(s1935,plain,
( ~ spl3_71
| spl3_399
| spl3_160
| ~ spl3_24
| ~ spl3_8
| spl3_5
| ~ spl3_18 ),
inference(rat,[],[s836,s837,s833,s825,s802,s1328,s1023,s1294,s549,s945,s946,s1450,s935,s1366,s1934,s1761,s830,s204]) ).
cnf(s1936,plain,
( spl3_399
| spl3_160
| ~ spl3_24
| ~ spl3_8
| spl3_5
| ~ spl3_18 ),
inference(rat,[],[s802,s913,s1023,s558,s549,s1279,s946,s605,s1225,s1229,s42,s1935,s1761,s830,s204,s1929]) ).
cnf(s1937,plain,
( spl3_49
| ~ spl3_18 ),
inference(rat,[],[s925,s952,s945,s1155,s1294,s1148,s1328,s180,s1185,s1324,s1194,s977,s42,s61,s230,s854,s1653,s1654,s27,s860,s104,s1931,s204,s1929]) ).
cnf(s1938,plain,
( ~ spl3_8
| ~ spl3_310
| ~ spl3_260
| spl3_399
| spl3_160
| spl3_5
| spl3_3 ),
inference(rat,[],[s847,s1042,s123,s1050,s1389,s1449,s339,s1427,s302,s14,s1366,s1936,s41,s1156,s9,s10,s16,s1089]) ).
cnf(s1939,plain,
( spl3_8
| ~ spl3_28
| ~ spl3_51 ),
inference(rat,[],[s592,s339,s1528,s324,s155,s61,s566,s977,s1194,s1539,s839,s1530,s4,s852,s1929,s104,s1931,s204]) ).
cnf(s1940,plain,
( spl3_310
| spl3_160
| ~ spl3_71
| ~ spl3_18 ),
inference(rat,[],[s1328,s825,s1294,s837,s945,s1052,s925,s833,s952,s802,s938,s1023,s178,s555,s204]) ).
cnf(s1941,plain,
( spl3_399
| spl3_160
| ~ spl3_71
| spl3_5
| spl3_3 ),
inference(rat,[],[s1938,s1934,s1939,s16,s1089,s28,s29,s1940,s9,s10]) ).
cnf(s1942,plain,
( spl3_160
| ~ spl3_71
| spl3_5
| spl3_3
| ~ spl3_2 ),
inference(rat,[],[s418,s417,s421,s1941,s1937,s9,s10]) ).
cnf(s1943,plain,
( ~ spl3_160
| spl3_5
| spl3_69 ),
inference(rat,[],[s1088,s1366,s664,s4,s311,s839,s1044,s1539,s758,s174,s442,s302,s761,s766,s1462,s16,s438,s794,s1669,s427,s436,s28,s29,s104,s1932,s204]) ).
cnf(s1944,plain,
( spl3_5
| spl3_3
| ~ spl3_2 ),
inference(rat,[],[s417,s430,s1936,s1256,s14,s913,s1289,s558,s359,s1279,s608,s605,s1229,s1939,s42,s16,s1942,s1089,s1943,s28,s29,s41,s1156,s1937,s9,s10,s204,s104,s1929]) ).
cnf(s1945,plain,
( spl3_399
| spl3_1007
| ~ spl3_160
| ~ spl3_5 ),
inference(rat,[],[s126,s581,s590,s592,s1309,s1088,s1537,s319,s1538,s61,s961,s978,s450,s866,s62,s152,s1268,s142,s31,s176,s1241,s320,s1583,s1627,s1929]) ).
cnf(s1946,plain,
( spl3_3
| ~ spl3_2 ),
inference(rat,[],[s835,s1342,s837,s1404,s970,s1236,s593,s605,s1770,s1279,s1537,s558,s1381,s932,s913,s1256,s430,s417,s1945,s1278,s1456,s777,s309,s314,s150,s305,s1944,s1937,s1925,s9,s1745,s10,s289,s1929,s204]) ).
cnf(s1947,plain,
spl3_1,
inference(rat,[],[s800,s1528,s393,s592,s858,s339,s417,s324,s860,s16,s1654,s430,s766,s188,s155,s61,s776,s442,s884,s566,s977,s758,s105,s290,s790,s335,s398,s1946,s1,s408,s1929,s104,s1932,s204]) ).
cnf(s1948,plain,
spl3_516,
inference(rat,[],[s1571,s1947]) ).
cnf(s1949,plain,
spl3_69,
inference(rat,[],[s788,s1947]) ).
cnf(s1952,plain,
spl3_5,
inference(rat,[],[s30,s1947]) ).
cnf(s1953,plain,
spl3_68,
inference(rat,[],[s41,s1949]) ).
cnf(s1954,plain,
spl3_723,
inference(rat,[],[s1009,s1953]) ).
cnf(s1955,plain,
spl3_471,
inference(rat,[],[s829,s104,s1953]) ).
cnf(s1957,plain,
~ spl3_721,
inference(rat,[],[s1619,s1954]) ).
cnf(s1958,plain,
~ spl3_1008,
inference(rat,[],[s1616,s1933,s1929,s1954]) ).
cnf(s1959,plain,
~ spl3_472,
inference(rat,[],[s269,s104,s1955]) ).
cnf(s1963,plain,
~ spl3_722,
inference(rat,[],[s835,s1957]) ).
cnf(s1964,plain,
~ spl3_58,
inference(rat,[],[s1541,s1958]) ).
cnf(s1965,plain,
~ spl3_508,
inference(rat,[],[s1169,s1958]) ).
cnf(s1966,plain,
~ spl3_259,
inference(rat,[],[s874,s104,s1959]) ).
cnf(s1969,plain,
~ spl3_989,
inference(rat,[],[s837,s1963]) ).
cnf(s1971,plain,
spl3_59,
inference(rat,[],[s36,s1964]) ).
cnf(s1972,plain,
~ spl3_520,
inference(rat,[],[s819,s1965]) ).
cnf(s1973,plain,
~ spl3_109,
inference(rat,[],[s450,s1966]) ).
cnf(s1975,plain,
~ spl3_504,
inference(rat,[],[s970,s204,s1969]) ).
cnf(s1978,plain,
spl3_400,
inference(rat,[],[s344,s1948,s1971]) ).
cnf(s1983,plain,
~ spl3_489,
inference(rat,[],[s1078,s1952,s1972]) ).
cnf(s1986,plain,
~ spl3_108,
inference(rat,[],[s62,s1929,s1973]) ).
cnf(s1987,plain,
spl3_306,
inference(rat,[],[s597,s1975]) ).
cnf(s1991,plain,
spl3_399,
inference(rat,[],[s1627,s1978]) ).
cnf(s1995,plain,
spl3_18,
inference(rat,[],[s393,s1983]) ).
cnf(s2000,plain,
spl3_981,
inference(rat,[],[s985,s1991,s1987]) ).
cnf(s2007,plain,
spl3_1000,
inference(rat,[],[s990,s2000]) ).
cnf(s2013,plain,
spl3_760,
inference(rat,[],[s1155,s2007]) ).
cnf(s2014,plain,
spl3_523,
inference(rat,[],[s1024,s2007]) ).
cnf(s2016,plain,
spl3_999,
inference(rat,[],[s952,s1995,s2013]) ).
cnf(s2018,plain,
~ spl3_614,
inference(rat,[],[s882,s1986,s2014]) ).
cnf(s2023,plain,
$false,
inference(rat,[],[s925,s2016,s2018]) ).
fof(f16452,plain,
$false,
inference(avatar_sat_refutation,[],[s2023]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO167+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n001.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 07:26:30 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.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
% 11.32/2.50 % (3219667)Detected formulas, will run a generic FOF schedule.
% 11.32/2.50 % (3219672)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=382292612:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.32/2.50 % (3219677)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2609721785:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.32/2.50 % (3219674)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=2659048322:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.32/2.50 % (3219673)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=1817144216:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.32/2.50 % (3219678)dis-21_1_sil=8000:lcm=predicate:random_seed=1385862745: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)
% 11.32/2.50 % (3219676)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2728145753:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.32/2.50 % (3219675)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=292864816:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.32/2.50 % (3219676)Refutation not found, incomplete strategy
% 11.32/2.50 % (3219676)------------------------------
% 11.32/2.50 % (3219676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.50 % (3219676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.50 % (3219676)CaDiCaL version: 2.1.3
% 11.32/2.50 % (3219675)Refutation not found, incomplete strategy
% 11.32/2.50 % (3219675)------------------------------
% 11.32/2.50 % (3219675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.50 % (3219676)Termination reason: Refutation not found, incomplete strategy
% 11.32/2.50 % (3219676)Time elapsed: 0.001 s
% 11.32/2.50 % (3219676)Peak memory usage: 86 MB
% 11.32/2.50 % (3219675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.50 % (3219675)CaDiCaL version: 2.1.3
% 11.32/2.50 % (3219675)Termination reason: Refutation not found, incomplete strategy
% 11.32/2.50 % (3219675)Time elapsed: 0.001 s
% 11.32/2.50 % (3219675)Peak memory usage: 86 MB
% 11.32/2.50 % (3219678)Instruction limit reached!
% 11.32/2.50 % (3219678)------------------------------
% 11.32/2.50 % (3219678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.50 % (3219678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.50 % (3219678)CaDiCaL version: 2.1.3
% 11.32/2.50 % (3219678)Termination reason: Instruction limit
% 11.32/2.50 % (3219678)Termination phase: Saturation
% 11.32/2.50 % (3219678)Time elapsed: 0.067 s
% 11.32/2.50 % (3219678)Peak memory usage: 88 MB
% 11.32/2.50 % (3219678)Instructions burned: 129 (million)
% 11.32/2.50 % (3219677)Instruction limit reached!
% 11.32/2.50 % (3219677)------------------------------
% 11.32/2.50 % (3219677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.50 % (3219677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.50 % (3219677)CaDiCaL version: 2.1.3
% 11.32/2.50 % (3219677)Termination reason: Instruction limit
% 11.32/2.50 % (3219677)Termination phase: Saturation
% 11.32/2.50 % (3219677)Time elapsed: 0.075 s
% 11.32/2.50 % (3219677)Peak memory usage: 88 MB
% 11.32/2.50 % (3219677)Instructions burned: 140 (million)
% 11.32/2.50 % (3219687)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2920998263:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.32/2.50 % (3219686)lrs+10_1_sil=8000:sp=occurrence:random_seed=1121187939:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.32/2.50 % (3219687)Refutation not found, incomplete strategy
% 11.32/2.50 % (3219687)------------------------------
% 11.32/2.50 % (3219687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.50 % (3219687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.50 % (3219687)CaDiCaL version: 2.1.3
% 11.32/2.50 % (3219687)Termination reason: Refutation not found, incomplete strategy
% 11.32/2.50 % (3219687)Time elapsed: 0.001 s
% 11.32/2.50 % (3219687)Peak memory usage: 87 MB
% 10.31/2.71 % (3219686)Refutation not found, incomplete strategy
% 10.31/2.71 % (3219686)------------------------------
% 10.31/2.71 % (3219686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.71 % (3219686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.71 % (3219686)CaDiCaL version: 2.1.3
% 10.31/2.71 % (3219686)Termination reason: Refutation not found, incomplete strategy
% 10.31/2.71 % (3219686)Time elapsed: 0.013 s
% 10.31/2.71 % (3219686)Peak memory usage: 88 MB
% 10.31/2.71 % (3219686)Instructions burned: 20 (million)
% 10.31/2.71 % (3219676)------------------------------
% 10.31/2.71 % (3219676)------------------------------
% 10.31/2.71 % (3219675)------------------------------
% 10.31/2.71 % (3219675)------------------------------
% 10.31/2.71 % (3219690)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1571256198:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 10.31/2.71 % (3219690)Refutation not found, incomplete strategy
% 10.31/2.71 % (3219690)------------------------------
% 10.31/2.71 % (3219690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.71 % (3219690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.71 % (3219690)CaDiCaL version: 2.1.3
% 10.31/2.71 % (3219690)Termination reason: Refutation not found, incomplete strategy
% 10.31/2.71 % (3219690)Time elapsed: 0.0000 s
% 10.31/2.71 % (3219690)Peak memory usage: 87 MB
% 10.31/2.71 % (3219691)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=581265404:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 10.31/2.71 % (3219687)------------------------------
% 10.31/2.71 % (3219687)------------------------------
% 10.31/2.71 % (3219686)------------------------------
% 10.31/2.71 % (3219686)------------------------------
% 10.31/2.71 % (3219690)------------------------------
% 10.31/2.71 % (3219690)------------------------------
% 10.31/2.71 % (3219691)Instruction limit reached!
% 10.31/2.71 % (3219691)------------------------------
% 10.31/2.71 % (3219691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.71 % (3219691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.71 % (3219691)CaDiCaL version: 2.1.3
% 10.31/2.71 % (3219691)Termination reason: Instruction limit
% 10.31/2.71 % (3219691)Termination phase: Saturation
% 10.31/2.71 % (3219691)Time elapsed: 0.123 s
% 10.31/2.71 % (3219691)Peak memory usage: 93 MB
% 10.31/2.71 % (3219691)Instructions burned: 248 (million)
% 10.31/2.71 % (3219694)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4114903781:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 10.31/2.71 % (3219694)Refutation not found, incomplete strategy
% 10.31/2.71 % (3219694)------------------------------
% 10.31/2.71 % (3219694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.71 % (3219694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.71 % (3219694)CaDiCaL version: 2.1.3
% 10.31/2.71 % (3219694)Termination reason: Refutation not found, incomplete strategy
% 10.31/2.71 % (3219694)Time elapsed: 0.001 s
% 10.31/2.71 % (3219694)Peak memory usage: 87 MB
% 10.31/2.71 % (3219694)Instructions burned: 1 (million)
% 10.31/2.71 % (3219695)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2538276108:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 10.31/2.71 % (3219696)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2196033069:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 10.31/2.71 % (3219697)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1826684604:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 10.31/2.71 % (3219696)Instruction limit reached!
% 10.31/2.71 % (3219696)------------------------------
% 10.31/2.71 % (3219696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.71 % (3219696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.71 % (3219696)CaDiCaL version: 2.1.3
% 10.31/2.71 % (3219696)Termination reason: Instruction limit
% 10.31/2.71 % (3219696)Termination phase: Saturation
% 10.31/2.71 % (3219696)Time elapsed: 0.060 s
% 10.31/2.71 % (3219696)Peak memory usage: 88 MB
% 10.31/2.71 % (3219696)Instructions burned: 113 (million)
% 10.31/2.71 % (3219697)Instruction limit reached!
% 10.31/2.71 % (3219697)------------------------------
% 10.31/2.71 % (3219697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.71 % (3219697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.71 % (3219697)CaDiCaL version: 2.1.3
% 10.31/2.71 % (3219697)Termination reason: Instruction limit
% 10.31/2.71 % (3219697)Termination phase: Saturation
% 10.31/2.71 % (3219697)Time elapsed: 0.058 s
% 10.31/2.71 % (3219697)Peak memory usage: 88 MB
% 10.31/2.71 % (3219697)Instructions burned: 128 (million)
% 10.31/2.71 % (3219694)------------------------------
% 10.31/2.71 % (3219694)------------------------------
% 10.31/2.71 % (3219703)lrs+10_1_sil=8000:sp=occurrence:random_seed=4002927052:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 10.31/2.71 % (3219702)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3220335077:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 10.31/2.71 % (3219702)Refutation not found, incomplete strategy
% 10.31/2.71 % (3219702)------------------------------
% 10.31/2.71 % (3219702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.71 % (3219702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.71 % (3219702)CaDiCaL version: 2.1.3
% 10.31/2.71 % (3219702)Termination reason: Refutation not found, incomplete strategy
% 10.31/2.71 % (3219702)Time elapsed: 0.001 s
% 10.31/2.71 % (3219702)Peak memory usage: 87 MB
% 10.31/2.71 % (3219704)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3085250887:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 10.31/2.71 % (3219704)Refutation not found, incomplete strategy
% 10.31/2.71 % (3219704)------------------------------
% 10.31/2.71 % (3219704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.71 % (3219704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.71 % (3219704)CaDiCaL version: 2.1.3
% 10.31/2.71 % (3219704)Termination reason: Refutation not found, incomplete strategy
% 10.31/2.71 % (3219704)Time elapsed: 0.002 s
% 10.31/2.71 % (3219704)Peak memory usage: 88 MB
% 10.31/2.71 % (3219704)Instructions burned: 1 (million)
% 10.31/2.71 % (3219702)------------------------------
% 10.31/2.71 % (3219702)------------------------------
% 10.31/2.71 % (3219703)Instruction limit reached!
% 10.31/2.71 % (3219703)------------------------------
% 10.31/2.71 % (3219703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.71 % (3219703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.71 % (3219703)CaDiCaL version: 2.1.3
% 10.31/2.71 % (3219703)Termination reason: Instruction limit
% 10.31/2.71 % (3219703)Termination phase: Saturation
% 10.31/2.71 % (3219703)Time elapsed: 0.257 s
% 10.31/2.71 % (3219703)Peak memory usage: 100 MB
% 10.31/2.71 % (3219703)Instructions burned: 907 (million)
% 10.31/2.71 % (3219709)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2724064540:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 10.31/2.71 % (3219704)------------------------------
% 10.31/2.71 % (3219704)------------------------------
% 10.31/2.71 % (3219709)Instruction limit reached!
% 10.31/2.71 % (3219709)------------------------------
% 10.31/2.71 % (3219709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.71 % (3219709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.71 % (3219709)CaDiCaL version: 2.1.3
% 10.31/2.71 % (3219709)Termination reason: Instruction limit
% 10.31/2.71 % (3219709)Termination phase: Saturation
% 10.31/2.71 % (3219709)Time elapsed: 0.038 s
% 10.31/2.71 % (3219709)Peak memory usage: 89 MB
% 10.31/2.71 % (3219709)Instructions burned: 138 (million)
% 10.31/2.71 % (3219708)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1190966610:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 10.31/2.71 % (3219672)First to succeed.
% 10.31/2.71 % (3219672)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3219667"
% 10.31/2.71 % (3219712)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2448372899:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 10.31/2.71 % (3219711)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1442783032:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 10.31/2.71 % (3219711)Refutation not found, incomplete strategy
% 10.31/2.71 % (3219711)------------------------------
% 10.31/2.71 % (3219711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.71 % (3219711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.71 % (3219711)CaDiCaL version: 2.1.3
% 10.31/2.71 % (3219711)Termination reason: Refutation not found, incomplete strategy
% 10.31/2.71 % (3219711)Time elapsed: 0.002 s
% 10.31/2.71 % (3219711)Peak memory usage: 88 MB
% 10.31/2.71 % (3219711)Instructions burned: 1 (million)
% 10.31/2.71 % (3219672)Refutation found. Thanks to Tanya!
% 10.31/2.71 % SZS status Theorem for theBenchmark
% 10.31/2.71 % SZS output start Proof for theBenchmark
% See solution above
% 13.54/2.81 % (3219672)------------------------------
% 13.54/2.81 % (3219672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.54/2.81 % (3219672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.54/2.81 % (3219672)CaDiCaL version: 2.1.3
% 13.54/2.81 % (3219672)Termination reason: Refutation
% 13.54/2.81 % (3219672)Time elapsed: 1.450 s
% 13.54/2.81 % (3219672)Peak memory usage: 143 MB
% 13.54/2.81 % (3219672)Instructions burned: 2441 (million)
% 13.54/2.81 % (3219672)------------------------------
% 13.54/2.81 % (3219672)------------------------------
% 13.54/2.81 % (3219667)Success in time 1.838 s
% 13.54/2.81 % Vampire exiting
%------------------------------------------------------------------------------